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