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

( P_{1}[x] & ( for a being set holds

( a in $1 iff ex y being Element of F_{3}() st

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

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 y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } 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 y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] }
_{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 y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } ,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, A10, A7, XBOOLE_0:def 10; :: thesis: verum

( P

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

( a = F

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

A2: { F

proof

A7:
{ ("\/" ( { 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)
and

A4: P_{1}[x]
and

A5: P_{2}[y]
;

set A1 = { F_{4}(x,y9) where y9 is Element of F_{3}() : P_{2}[y9] } ;

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

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

a in A1 by A3, A5;

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

end;assume a in { F

then consider x being Element of F

A3: a = F

A4: P

A5: 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}(x,y9) where y9 is Element of F_{3}() : P_{2}[y9] } or b in the carrier of F_{1}() )

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

then ex y9 being Element of F_{3}() st

( b = F_{4}(x,y9) & P_{2}[y9] )
;

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

end;assume b in { F

then ex y9 being Element of F

( b = F

hence b in the carrier of F

S

proof

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

( a in A1 iff ex y being Element of F_{3}() st

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

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

( a in A1 iff ex y being Element of F_{3}() st

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

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

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

thus ( a in A1 iff ex y being Element of F_{3}() st

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

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

( a = F

thus P

( a in A1 iff ex y being Element of F

( a = F

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

( a = F

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

( a = F

a in A1 by A3, A5;

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

proof

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

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

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

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

A9: P_{1}[x]
;

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 x being Element of F

A8: a = "\/" ( { F

A9: P

ex A1 being Subset of F

( a = "\/" (A1,F

proof

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

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

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

( a = "\/" (A1,F_{1}()) & S_{1}[A1] )
by A8; :: 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 y is Element of F_{3}() : P_{2}[y] } or b in the carrier of F_{1}() )

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

then ex y being Element of F_{3}() st

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

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

end;assume b in { F

then ex y being Element of F

( b = F

hence b in the carrier of F

S

proof

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

( a in A1 iff ex y being Element of F_{3}() st

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

thus P_{1}[x]
by A9; :: thesis: for a being set holds

( a in A1 iff ex y being Element of F_{3}() st

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

thus for a being set holds

( a in A1 iff ex y being Element of F_{3}() st

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

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

( a = F

thus P

( a in A1 iff ex y being Element of F

( a = F

thus for a being set holds

( a in A1 iff ex y 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 y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } )

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

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

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

A12: S_{1}[A1]
;

consider x being Element of F_{2}() such that

A13: P_{1}[x]
and

A14: for a being set holds

( a in A1 iff ex y being Element of F_{3}() st

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

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

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

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

then consider A1 being Subset of F

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

A12: S

consider x being Element of F

A13: P

A14: for a being set holds

( a in A1 iff ex y being Element of F

( a = F

now :: thesis: for a being object holds

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

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 y is Element of F_{3}() : P_{2}[y] } )

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

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

hence ( a in A1 iff a in { F_{4}(x,y) where y is Element of F_{3}() : P_{2}[y] } )
by A14; :: 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

A15: a in A1 and

A16: 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

A17: A1 = A2 and

A18: S_{1}[A2]
by A16;

consider x being Element of F_{2}() such that

A19: P_{1}[x]
and

A20: for a being set holds

( a in A2 iff ex y being Element of F_{3}() st

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

ex y being Element of F_{3}() st

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

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 A19; :: thesis: verum

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

then consider A1 being set such that

A15: a in A1 and

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

consider A2 being Subset of F

A17: A1 = A2 and

A18: S

consider x being Element of F

A19: P

A20: for a being set holds

( a in A2 iff ex y being Element of F

( a = F

ex y being Element of F

( a = F

hence a in { F

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