set Q = F1();
set X = F3();
set Y = F4();
set Z = { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ;
set W = { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ;
set S = { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ;
A1: { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } = { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
proof
thus { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } c= { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } c= { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } or x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } )
assume x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ; :: thesis: x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
then consider V being Subset of F1() such that
A2: x = "\/" V and
A3: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ;
ex a being Element of F1() st
( V = { F2(a,b) where b is Element of F1() : b in F4() } & a in F3() ) by A3;
hence x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } or x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } )
assume x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ; :: thesis: x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
then consider a being Element of F1() such that
A4: x = "\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1()) and
A5: a in F3() ;
A6: { F2(a,b) where b is Element of F1() : b in F4() } c= H1(F1())
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { F2(a,b) where b is Element of F1() : b in F4() } or y in H1(F1()) )
assume y in { F2(a,b) where b is Element of F1() : b in F4() } ; :: thesis: y in H1(F1())
then ex b being Element of F1() st
( y = F2(a,b) & b in F4() ) ;
hence y in H1(F1()) ; :: thesis: verum
end;
{ F2(a,c) where c is Element of F1() : c in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by A5;
hence x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } by A4, A6; :: thesis: verum
end;
A7: { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } = union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
proof
thus { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } c= union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def 10 :: thesis: union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } or x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } )
assume x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ; :: thesis: x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
then consider a, b being Element of F1() such that
A8: ( x = F2(a,b) & a in F3() & b in F4() ) ;
( x in { F2(a,c) where c is Element of F1() : c in F4() } & { F2(a,d) where d is Element of F1() : d in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ) by A8;
hence x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } )
assume x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; :: thesis: x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
then consider V being set such that
A9: x in V and
A10: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def 4;
consider a being Element of F1() such that
A11: V = { F2(a,b) where b is Element of F1() : b in F4() } and
A12: a in F3() by A10;
ex b being Element of F1() st
( x = F2(a,b) & b in F4() ) by A9, A11;
hence x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } by A12; :: thesis: verum
end;
{ { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= bool H1(F1())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in bool H1(F1()) )
reconsider xx = x as set by TARSKI:1;
assume x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; :: thesis: x in bool H1(F1())
then consider a being Element of F1() such that
A13: x = { F2(a,b) where b is Element of F1() : b in F4() } and
a in F3() ;
xx c= H1(F1())
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in H1(F1()) )
assume y in xx ; :: thesis: y in H1(F1())
then ex b being Element of F1() st
( y = F2(a,b) & b in F4() ) by A13;
hence y in H1(F1()) ; :: thesis: verum
end;
hence x in bool H1(F1()) ; :: thesis: verum
end;
hence "\/" ( { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ,F1()) = "\/" ( { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ,F1()) by A1, A7, LATTICE3:48; :: thesis: verum