let E be non empty set ; for e being Element of E
for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let e be Element of E; for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let f be Function of VAR,E; ( E is epsilon-transitive implies Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) )
set H = All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))));
set v = f / ((x. 1),e);
set S = Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)));
Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) =
(Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)}
by ZF_LANG1:62
.=
((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)}
by ZF_LANG1:64
.=
((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)}
by ZF_LANG1:59
.=
({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)}
by ZF_LANG1:59
.=
({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)})
by XBOOLE_1:42
.=
({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)}
by ZFMISC_1:17, ZF_LANG1:76
.=
{(x. 0)} \/ {(x. 1)}
by ZFMISC_1:17, ZF_LANG1:76
.=
{(x. 0),(x. 1)}
by ENUMSET1:1
;
then
x. 0 in Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))))
by TARSKI:def 2;
then A1:
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = { m where m is Element of E : E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) }
by Def1;
assume A2:
for X being set st X in E holds
X c= E
; ORDINAL1:def 2 Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
thus
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) c= E /\ (bool e)
XBOOLE_0:def 10 E /\ (bool e) c= Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))proof
let u be
object ;
TARSKI:def 3 ( not u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) or u in E /\ (bool e) )
assume
u in Section (
(All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),
(f / ((x. 1),e)))
;
u in E /\ (bool e)
then consider m being
Element of
E such that A3:
u = m
and A4:
E,
(f / ((x. 1),e)) / (
(x. 0),
m)
|= All (
(x. 2),
(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))
by A1;
A5:
m c= E
by A2;
m c= e
proof
let u1 be
object ;
TARSKI:def 3 ( not u1 in m or u1 in e )
assume A6:
u1 in m
;
u1 in e
then reconsider u1 =
u1 as
Element of
E by A5;
A7:
(((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 2) = u1
by FUNCT_7:128;
A8:
E,
((f / ((x. 1),e)) / ((x. 0),m)) / (
(x. 2),
u1)
|= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))
by A4, ZF_LANG1:71;
A9:
(
(((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) &
(f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) )
by FUNCT_7:32, ZF_LANG1:76;
(
m = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) &
(((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) )
by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
then
E,
((f / ((x. 1),e)) / ((x. 0),m)) / (
(x. 2),
u1)
|= (x. 2) 'in' (x. 0)
by A6, A7, ZF_MODEL:13;
then
(
(f / ((x. 1),e)) . (x. 1) = e &
E,
((f / ((x. 1),e)) / ((x. 0),m)) / (
(x. 2),
u1)
|= (x. 2) 'in' (x. 1) )
by A8, FUNCT_7:128, ZF_MODEL:18;
hence
u1 in e
by A7, A9, ZF_MODEL:13;
verum
end;
then
u in bool e
by A3, ZFMISC_1:def 1;
hence
u in E /\ (bool e)
by A3, XBOOLE_0:def 4;
verum
end;
let u be object ; TARSKI:def 3 ( not u in E /\ (bool e) or u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) )
assume A10:
u in E /\ (bool e)
; u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))
then A11:
u in bool e
by XBOOLE_0:def 4;
reconsider u = u as Element of E by A10, XBOOLE_0:def 4;
now for m being Element of E holds E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))A12:
(f / ((x. 1),e)) . (x. 1) = e
by FUNCT_7:128;
let m be
Element of
E;
E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))A13:
(((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 2) = m
by FUNCT_7:128;
A14:
(
u = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) &
(((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) )
by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
A15:
(
(((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) &
(f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) )
by FUNCT_7:32, ZF_LANG1:76;
now ( E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 0) implies E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) )assume
E,
((f / ((x. 1),e)) / ((x. 0),u)) / (
(x. 2),
m)
|= (x. 2) 'in' (x. 0)
;
E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1)then
m in u
by A13, A14, ZF_MODEL:13;
hence
E,
((f / ((x. 1),e)) / ((x. 0),u)) / (
(x. 2),
m)
|= (x. 2) 'in' (x. 1)
by A11, A13, A15, A12, ZF_MODEL:13;
verum end; hence
E,
((f / ((x. 1),e)) / ((x. 0),u)) / (
(x. 2),
m)
|= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))
by ZF_MODEL:18;
verum end;
then
E,(f / ((x. 1),e)) / ((x. 0),u) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))
by ZF_LANG1:71;
hence
u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))
by A1; verum