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
object ;
TARSKI:def 3 ( 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] ) }
;
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()
then reconsider A1 =
{ F4(x,y9) where y9 is Element of F3() : P2[y9] } as
Subset of
F1() ;
S1[
A1]
proof
take
x
;
( 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;
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 ;
( 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] ) )
;
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;
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
object ;
TARSKI:def 3 ( 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] }
;
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()
then reconsider A1 =
{ F4(x,y) where y is Element of F3() : P2[y] } as
Subset of
F1() ;
S1[
A1]
proof
take
x
;
( 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;
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] ) )
;
verum
end;
hence
ex
A1 being
Subset of
F1() st
(
a = "\/" (
A1,
F1()) &
S1[
A1] )
by A8;
verum
end;
hence
a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] }
;
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
object ;
TARSKI:def 3 ( 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] }
;
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 for a being object holds
( a in A1 iff a in { F4(x,y) where y is Element of F3() : P2[y] } )let a be
object ;
( 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;
verum end;
then
A1 = { F4(x,y) where y is Element of F3() : P2[y] }
by TARSKI:2;
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;
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 ;
TARSKI:def 3 ( 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] }
;
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;
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 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; verum