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 A1:
( X is closed_wrt_A1-A7 & 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
then A2:
X is closed_wrt_A7
by Def13;
A3:
X is closed_wrt_A4
by A1, Def13;
set f = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]};
set F = { {[(1-element_of V),x]} where x is Element of V : x in a } ;
set Z = { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ;
{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} in X
proof
A5:
(
0-element_of V in X &
1-element_of V in X )
by A1, Lm13;
then A6:
[(0-element_of V),(1-element_of V)] in X
by A1, Th6;
[(1-element_of V),(1-element_of V)] in X
by A1, A5, Th6;
hence
{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} in X
by A1, A6, Th6;
:: thesis: verum
end;
then A7:
{{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} in X
by A1, Th2;
set f' = {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}};
A8:
{ {[(1-element_of V),x]} where x is Element of V : x in a } in X
proof
1-element_of V in X
by A1, Lm13;
then A10:
{(1-element_of V)} in X
by A1, Th2;
reconsider s =
{(1-element_of V)} as
Element of
V ;
{ {[(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 }
let p be
set ;
:: 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 A12:
(
p = {[y,x]} &
y in s &
x in a )
;
p = {[(1-element_of V),x]}
by A12, TARSKI:def 1;
hence
p in { {[(1-element_of V),x]} where x is Element of V : x in a }
by A12;
:: thesis: verum
end;
hence
{ {[(1-element_of V),x]} where x is Element of V : x in a } in X
by A1, A3, A10, Def9;
:: thesis: verum
end;
then reconsider F' = { {[(1-element_of V),x]} where x is Element of V : x in a } as Element of V ;
{ {[(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 F' ) }
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 F' ) }
:: 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 F' ) } c= { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } proof
let p be
set ;
:: 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 F' ) } )
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 F' ) }
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 x' =
{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} as
Element of
V ;
reconsider y =
{[(1-element_of V),x]} as
Element of
V ;
A14:
y in F'
by A13;
A15:
x' in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}}
by TARSKI:def 1;
p = x' (#) 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 F' ) }
by A14, A15;
:: thesis: verum
end;
let p be
set ;
:: 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 F' ) } 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 F' ) }
;
:: 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 A16:
(
p = x (#) y &
x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} &
y in F' )
;
A17:
x = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}
by A16, TARSKI:def 1;
consider x' being
Element of
V such that A18:
(
y = {[(1-element_of V),x']} &
x' in a )
by A16;
p = {[(0-element_of V),x'],[(1-element_of V),x']}
by A16, A17, A18, 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;
hence
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X
by A2, A7, A8, Def12; :: thesis: verum