defpred S_{1}[ set ] means ex y being Element of F_{3}() st

( P_{2}[y] & ( for a being set holds

( a in $1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) ) ) );

A1: "\/" ( { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] } ,F_{1}()) = "\/" ((union { A where A is Subset of F_{1}() : S_{1}[A] } ),F_{1}())
from YELLOW_3:sch 5();

A2: { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } c= union { A where A is Subset of F_{1}() : S_{1}[A] }
_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] } c= { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] }
_{1}())) where A is Subset of F_{1}() : S_{1}[A] } c= { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] }
_{1}() : S_{1}[A] } c= { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) }
_{1}() : S_{1}[A] } = { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) }
by A2;

hence "\/" ( { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}()) = "\/" ( { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } ,F_{1}())
by A1, A9, A6, XBOOLE_0:def 10; :: thesis: verum

( P

( a in $1 iff ex x being Element of F

( a = F

A1: "\/" ( { ("\/" (A,F

A2: { F

proof

A6:
{ ("\/" ( { F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } or a in union { A where A is Subset of F_{1}() : S_{1}[A] } )

assume a in { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) }
; :: thesis: a in union { A where A is Subset of F_{1}() : S_{1}[A] }

then consider x being Element of F_{2}(), y being Element of F_{3}() such that

A3: ( a = F_{4}(x,y) & P_{1}[x] )
and

A4: P_{2}[y]
;

set A1 = { F_{4}(x9,y) where x9 is Element of F_{2}() : P_{1}[x9] } ;

{ F_{4}(x9,y) where x9 is Element of F_{2}() : P_{1}[x9] } c= the carrier of F_{1}()
_{4}(x9,y) where x9 is Element of F_{2}() : P_{1}[x9] } as Subset of F_{1}() ;

S_{1}[A1]
_{1}() : S_{1}[A] }
;

a in A1 by A3;

hence a in union { A where A is Subset of F_{1}() : S_{1}[A] }
by A5, TARSKI:def 4; :: thesis: verum

end;assume a in { F

then consider x being Element of F

A3: ( a = F

A4: P

set A1 = { F

{ F

proof

then reconsider A1 = { F
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { F_{4}(x9,y) where x9 is Element of F_{2}() : P_{1}[x9] } or b in the carrier of F_{1}() )

assume b in { F_{4}(x9,y) where x9 is Element of F_{2}() : P_{1}[x9] }
; :: thesis: b in the carrier of F_{1}()

then ex x9 being Element of F_{2}() st

( b = F_{4}(x9,y) & P_{1}[x9] )
;

hence b in the carrier of F_{1}()
; :: thesis: verum

end;assume b in { F

then ex x9 being Element of F

( b = F

hence b in the carrier of F

S

proof

then A5:
A1 in { A where A is Subset of F
take
y
; :: thesis: ( P_{2}[y] & ( for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) ) ) )

thus P_{2}[y]
by A4; :: thesis: for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )

let a be set ; :: thesis: ( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )

thus ( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )
; :: thesis: verum

end;( a in A1 iff ex x being Element of F

( a = F

thus P

( a in A1 iff ex x being Element of F

( a = F

let a be set ; :: thesis: ( a in A1 iff ex x being Element of F

( a = F

thus ( a in A1 iff ex x being Element of F

( a = F

a in A1 by A3;

hence a in union { A where A is Subset of F

proof

A9:
{ ("\/" (A,F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] } or a in { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] } )

assume a in { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] }
; :: thesis: a in { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] }

then consider y being Element of F_{3}() such that

A7: a = "\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())
and

A8: P_{2}[y]
;

ex A1 being Subset of F_{1}() st

( a = "\/" (A1,F_{1}()) & S_{1}[A1] )
_{1}())) where A is Subset of F_{1}() : S_{1}[A] }
; :: thesis: verum

end;assume a in { ("\/" ( { F

then consider y being Element of F

A7: a = "\/" ( { F

A8: P

ex A1 being Subset of F

( a = "\/" (A1,F

proof

hence
a in { ("\/" (A,F
set A2 = { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ;

{ F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } c= the carrier of F_{1}()
_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } as Subset of F_{1}() ;

S_{1}[A1]
_{1}() st

( a = "\/" (A1,F_{1}()) & S_{1}[A1] )
by A7; :: thesis: verum

end;{ F

proof

then reconsider A1 = { F
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } or b in the carrier of F_{1}() )

assume b in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] }
; :: thesis: b in the carrier of F_{1}()

then ex x being Element of F_{2}() st

( b = F_{4}(x,y) & P_{1}[x] )
;

hence b in the carrier of F_{1}()
; :: thesis: verum

end;assume b in { F

then ex x being Element of F

( b = F

hence b in the carrier of F

S

proof

hence
ex A1 being Subset of F
take
y
; :: thesis: ( P_{2}[y] & ( for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) ) ) )

thus P_{2}[y]
by A8; :: thesis: for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )

thus for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )
; :: thesis: verum

end;( a in A1 iff ex x being Element of F

( a = F

thus P

( a in A1 iff ex x being Element of F

( a = F

thus for a being set holds

( a in A1 iff ex x being Element of F

( a = F

( a = "\/" (A1,F

proof

union { A where A is Subset of F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] } or a in { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] } )

assume a in { ("\/" (A,F_{1}())) where A is Subset of F_{1}() : S_{1}[A] }
; :: thesis: a in { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] }

then consider A1 being Subset of F_{1}() such that

A10: a = "\/" (A1,F_{1}())
and

A11: S_{1}[A1]
;

consider y being Element of F_{3}() such that

A12: P_{2}[y]
and

A13: for a being set holds

( a in A1 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )
by A11;

_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] }
by TARSKI:2;

hence a in { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] }
by A10, A12; :: thesis: verum

end;assume a in { ("\/" (A,F

then consider A1 being Subset of F

A10: a = "\/" (A1,F

A11: S

consider y being Element of F

A12: P

A13: for a being set holds

( a in A1 iff ex x being Element of F

( a = F

now :: thesis: for a being object holds

( a in A1 iff a in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } )

then
A1 = { F( a in A1 iff a in { F

let a be object ; :: thesis: ( a in A1 iff a in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } )

( a in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )
;

hence ( a in A1 iff a in { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } )
by A13; :: thesis: verum

end;( a in { F

( a = F

hence ( a in A1 iff a in { F

hence a in { ("\/" ( { F

proof

then
union { A where A is Subset of F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { A where A is Subset of F_{1}() : S_{1}[A] } or a in { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } )

assume a in union { A where A is Subset of F_{1}() : S_{1}[A] }
; :: thesis: a in { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) }

then consider A1 being set such that

A14: a in A1 and

A15: A1 in { A where A is Subset of F_{1}() : S_{1}[A] }
by TARSKI:def 4;

consider A2 being Subset of F_{1}() such that

A16: A1 = A2 and

A17: S_{1}[A2]
by A15;

consider y being Element of F_{3}() such that

A18: P_{2}[y]
and

A19: for a being set holds

( a in A2 iff ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] ) )
by A17;

ex x being Element of F_{2}() st

( a = F_{4}(x,y) & P_{1}[x] )
by A14, A16, A19;

hence a in { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) }
by A18; :: thesis: verum

end;assume a in union { A where A is Subset of F

then consider A1 being set such that

A14: a in A1 and

A15: A1 in { A where A is Subset of F

consider A2 being Subset of F

A16: A1 = A2 and

A17: S

consider y being Element of F

A18: P

A19: for a being set holds

( a in A2 iff ex x being Element of F

( a = F

ex x being Element of F

( a = F

hence a in { F

hence "\/" ( { ("\/" ( { F