let V be Universe; :: thesis: for a being Element of V
for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X
let a be Element of V; :: thesis: for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X
let X be Subclass of V; :: thesis: ( X is closed_wrt_A1-A7 & a in X implies { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X )
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X ; :: thesis: { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X
set f = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]};
A3: 1-element_of V in X by A1, Lm13;
then A4: [(1-element_of V),(1-element_of V)] in X by A1, Th6;
set F = { {[(1-element_of V),x]} where x is Element of V : x in a } ;
A5: X is closed_wrt_A4 by A1;
A6: { {[(1-element_of V),x]} where x is Element of V : x in a } in X
proof
reconsider s = {(1-element_of V)} as Element of V ;
A7: { {[(1-element_of V),x]} where x is Element of V : x in a } = { {[y,x]} where y, x is Element of V : ( y in s & x in a ) }
proof
thus { {[(1-element_of V),x]} where x is Element of V : x in a } c= { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } :: according to XBOOLE_0:def 10 :: thesis: { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } c= { {[(1-element_of V),x]} where x is Element of V : x in a }
proof
reconsider y = 1-element_of V as Element of V ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { {[(1-element_of V),x]} where x is Element of V : x in a } or p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } )
assume p in { {[(1-element_of V),x]} where x is Element of V : x in a } ; :: thesis: p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) }
then A8: ex x being Element of V st
( p = {[(1-element_of V),x]} & x in a ) ;
y in s by TARSKI:def 1;
hence p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } by A8; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } or p in { {[(1-element_of V),x]} where x is Element of V : x in a } )
assume p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } ; :: thesis: p in { {[(1-element_of V),x]} where x is Element of V : x in a }
then consider y, x being Element of V such that
A9: ( p = {[y,x]} & y in s ) and
A10: x in a ;
p = {[(1-element_of V),x]} by A9, TARSKI:def 1;
hence p in { {[(1-element_of V),x]} where x is Element of V : x in a } by A10; :: thesis: verum
end;
1-element_of V in X by A1, Lm13;
then {(1-element_of V)} in X by A1, Th2;
hence { {[(1-element_of V),x]} where x is Element of V : x in a } in X by A2, A5, A7; :: thesis: verum
end;
then reconsider F9 = { {[(1-element_of V),x]} where x is Element of V : x in a } as Element of V ;
set f9 = {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}};
set Z = { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ;
A11: { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } = { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) }
proof
thus { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } c= { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } :: according to XBOOLE_0:def 10 :: thesis: { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } c= { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a }
proof
reconsider x9 = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} as Element of V ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } or p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } )
A12: x9 in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} by TARSKI:def 1;
assume p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ; :: thesis: p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) }
then consider x being Element of V such that
A13: ( p = {[(0-element_of V),x],[(1-element_of V),x]} & x in a ) ;
reconsider y = {[(1-element_of V),x]} as Element of V ;
( y in F9 & p = x9 (#) y ) by A13, Lm14;
hence p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } by A12; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } or p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } )
assume p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } ; :: thesis: p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a }
then consider x, y being Element of V such that
A14: p = x (#) y and
A15: x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} and
A16: y in F9 ;
consider x9 being Element of V such that
A17: y = {[(1-element_of V),x9]} and
A18: x9 in a by A16;
x = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} by A15, TARSKI:def 1;
then p = {[(0-element_of V),x9],[(1-element_of V),x9]} by A14, A17, Lm14;
hence p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } by A18; :: thesis: verum
end;
0-element_of V in X by A1, Lm13;
then [(0-element_of V),(1-element_of V)] in X by A1, A3, Th6;
then {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} in X by A1, A4, Th6;
then A19: {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} in X by A1, Th2;
X is closed_wrt_A7 by A1;
hence { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X by A19, A6, A11; :: thesis: verum