defpred S1[ set ] means ex y being Element of F3() st
( P2[y] & ( for a being set holds
( a in $1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) );
A1: "\/" ( { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ,F1()) = "\/" ((union { A where A is Subset of F1() : S1[A] } ),F1()) from YELLOW_3:sch 5();
 A2: { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } c= union { A where A is Subset of F1() : S1[A] }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } or a in union { A where A is Subset of F1() : S1[A] } )
assume a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ; :: thesis: a in union { A where A is Subset of F1() : S1[A] }
then consider x being Element of F2(), y being Element of F3() such that
A3: ( a = F4(x,y) & P1[x] ) and
A4: P2[y] ;
set A1 = { F4(x9,y) where x9 is Element of F2() : P1[x9] } ;
{ F4(x9,y) where x9 is Element of F2() : P1[x9] } c= the carrier of F1()
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { F4(x9,y) where x9 is Element of F2() : P1[x9] } or b in the carrier of F1() )
assume b in { F4(x9,y) where x9 is Element of F2() : P1[x9] } ; :: thesis: b in the carrier of F1()
then ex x9 being Element of F2() st
( b = F4(x9,y) & P1[x9] ) ;
hence b in the carrier of F1() ; :: thesis: verum
end;
then reconsider A1 = { F4(x9,y) where x9 is Element of F2() : P1[x9] } as Subset of F1() ;
S1[A1]
proof
take y ; :: thesis: ( P2[y] & ( for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) )
thus P2[y] by A4; :: thesis: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
let a be set ; :: thesis: ( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
thus ( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ; :: thesis: verum
end;
then A5: A1 in { A where A is Subset of F1() : S1[A] } ;
a in A1 by A3;
hence a in union { A where A is Subset of F1() : S1[A] } by A5, TARSKI:def 4; :: thesis: verum
end;
A6: { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } c= { ("\/" (A,F1())) where A is Subset of F1() : S1[A] }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } or a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } )
assume a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ; :: thesis: a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] }
then consider y being Element of F3() such that
A7: a = "\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1()) and
A8: P2[y] ;
 ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] )
proof
set A2 = { F4(x,y) where x is Element of F2() : P1[x] } ;
{ F4(x,y) where x is Element of F2() : P1[x] } c= the carrier of F1()
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { F4(x,y) where x is Element of F2() : P1[x] } or b in the carrier of F1() )
assume b in { F4(x,y) where x is Element of F2() : P1[x] } ; :: thesis: b in the carrier of F1()
then ex x being Element of F2() st
( b = F4(x,y) & P1[x] ) ;
hence b in the carrier of F1() ; :: thesis: verum
end;
then reconsider A1 = { F4(x,y) where x is Element of F2() : P1[x] } as Subset of F1() ;
S1[A1]
proof
take y ; :: thesis: ( P2[y] & ( for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) )
thus P2[y] by A8; :: thesis: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
thus for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ; :: thesis: verum
end;
hence ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] ) by A7; :: thesis: verum
end;
hence a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; :: thesis: verum
end;
A9: { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } c= { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } or a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } )
assume a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; :: thesis: a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] }
then consider A1 being Subset of F1() such that
A10: a = "\/" (A1,F1()) and
A11: S1[A1] ;
consider y being Element of F3() such that
A12: P2[y] and
A13: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) by A11;
now :: thesis: for a being object holds
( a in A1 iff a in { F4(x,y) where x is Element of F2() : P1[x] } )
let a be object ; :: thesis: ( a in A1 iff a in { F4(x,y) where x is Element of F2() : P1[x] } )
( a in { F4(x,y) where x is Element of F2() : P1[x] } iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ;
hence ( a in A1 iff a in { F4(x,y) where x is Element of F2() : P1[x] } ) by A13; :: thesis: verum
end;
then A1 = { F4(x,y) where x is Element of F2() : P1[x] } by TARSKI:2;
hence a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } by A10, A12; :: thesis: verum
end;
union { A where A is Subset of F1() : S1[A] } c= { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { A where A is Subset of F1() : S1[A] } or a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } )
assume a in union { A where A is Subset of F1() : S1[A] } ; :: thesis: a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) }
then consider A1 being set such that
A14: a in A1 and
A15: A1 in { A where A is Subset of F1() : S1[A] } by TARSKI:def 4;
consider A2 being Subset of F1() such that
A16: A1 = A2 and
A17: S1[A2] by A15;
consider y being Element of F3() such that
A18: P2[y] and
A19: for a being set holds
( a in A2 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) by A17;
ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) by A14, A16, A19;
hence a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A18; :: thesis: verum
end;
then union { A where A is Subset of F1() : S1[A] } = { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A2;
hence "\/" ( { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) by A1, A9, A6, XBOOLE_0:def 10; :: thesis: verum