Step |
Hyp |
Ref |
Expression |
1 |
|
txval.1 |
|- B = ran ( x e. R , y e. S |-> ( x X. y ) ) |
2 |
|
txuni2.1 |
|- X = U. R |
3 |
|
txuni2.2 |
|- Y = U. S |
4 |
|
relxp |
|- Rel ( X X. Y ) |
5 |
2
|
eleq2i |
|- ( z e. X <-> z e. U. R ) |
6 |
|
eluni2 |
|- ( z e. U. R <-> E. r e. R z e. r ) |
7 |
5 6
|
bitri |
|- ( z e. X <-> E. r e. R z e. r ) |
8 |
3
|
eleq2i |
|- ( w e. Y <-> w e. U. S ) |
9 |
|
eluni2 |
|- ( w e. U. S <-> E. s e. S w e. s ) |
10 |
8 9
|
bitri |
|- ( w e. Y <-> E. s e. S w e. s ) |
11 |
7 10
|
anbi12i |
|- ( ( z e. X /\ w e. Y ) <-> ( E. r e. R z e. r /\ E. s e. S w e. s ) ) |
12 |
|
opelxp |
|- ( <. z , w >. e. ( X X. Y ) <-> ( z e. X /\ w e. Y ) ) |
13 |
|
reeanv |
|- ( E. r e. R E. s e. S ( z e. r /\ w e. s ) <-> ( E. r e. R z e. r /\ E. s e. S w e. s ) ) |
14 |
11 12 13
|
3bitr4i |
|- ( <. z , w >. e. ( X X. Y ) <-> E. r e. R E. s e. S ( z e. r /\ w e. s ) ) |
15 |
|
opelxp |
|- ( <. z , w >. e. ( r X. s ) <-> ( z e. r /\ w e. s ) ) |
16 |
|
eqid |
|- ( r X. s ) = ( r X. s ) |
17 |
|
xpeq1 |
|- ( x = r -> ( x X. y ) = ( r X. y ) ) |
18 |
17
|
eqeq2d |
|- ( x = r -> ( ( r X. s ) = ( x X. y ) <-> ( r X. s ) = ( r X. y ) ) ) |
19 |
|
xpeq2 |
|- ( y = s -> ( r X. y ) = ( r X. s ) ) |
20 |
19
|
eqeq2d |
|- ( y = s -> ( ( r X. s ) = ( r X. y ) <-> ( r X. s ) = ( r X. s ) ) ) |
21 |
18 20
|
rspc2ev |
|- ( ( r e. R /\ s e. S /\ ( r X. s ) = ( r X. s ) ) -> E. x e. R E. y e. S ( r X. s ) = ( x X. y ) ) |
22 |
16 21
|
mp3an3 |
|- ( ( r e. R /\ s e. S ) -> E. x e. R E. y e. S ( r X. s ) = ( x X. y ) ) |
23 |
|
vex |
|- r e. _V |
24 |
|
vex |
|- s e. _V |
25 |
23 24
|
xpex |
|- ( r X. s ) e. _V |
26 |
|
eqeq1 |
|- ( z = ( r X. s ) -> ( z = ( x X. y ) <-> ( r X. s ) = ( x X. y ) ) ) |
27 |
26
|
2rexbidv |
|- ( z = ( r X. s ) -> ( E. x e. R E. y e. S z = ( x X. y ) <-> E. x e. R E. y e. S ( r X. s ) = ( x X. y ) ) ) |
28 |
|
eqid |
|- ( x e. R , y e. S |-> ( x X. y ) ) = ( x e. R , y e. S |-> ( x X. y ) ) |
29 |
28
|
rnmpo |
|- ran ( x e. R , y e. S |-> ( x X. y ) ) = { z | E. x e. R E. y e. S z = ( x X. y ) } |
30 |
1 29
|
eqtri |
|- B = { z | E. x e. R E. y e. S z = ( x X. y ) } |
31 |
25 27 30
|
elab2 |
|- ( ( r X. s ) e. B <-> E. x e. R E. y e. S ( r X. s ) = ( x X. y ) ) |
32 |
22 31
|
sylibr |
|- ( ( r e. R /\ s e. S ) -> ( r X. s ) e. B ) |
33 |
|
elssuni |
|- ( ( r X. s ) e. B -> ( r X. s ) C_ U. B ) |
34 |
32 33
|
syl |
|- ( ( r e. R /\ s e. S ) -> ( r X. s ) C_ U. B ) |
35 |
34
|
sseld |
|- ( ( r e. R /\ s e. S ) -> ( <. z , w >. e. ( r X. s ) -> <. z , w >. e. U. B ) ) |
36 |
15 35
|
syl5bir |
|- ( ( r e. R /\ s e. S ) -> ( ( z e. r /\ w e. s ) -> <. z , w >. e. U. B ) ) |
37 |
36
|
rexlimivv |
|- ( E. r e. R E. s e. S ( z e. r /\ w e. s ) -> <. z , w >. e. U. B ) |
38 |
14 37
|
sylbi |
|- ( <. z , w >. e. ( X X. Y ) -> <. z , w >. e. U. B ) |
39 |
4 38
|
relssi |
|- ( X X. Y ) C_ U. B |
40 |
|
elssuni |
|- ( x e. R -> x C_ U. R ) |
41 |
40 2
|
sseqtrrdi |
|- ( x e. R -> x C_ X ) |
42 |
|
elssuni |
|- ( y e. S -> y C_ U. S ) |
43 |
42 3
|
sseqtrrdi |
|- ( y e. S -> y C_ Y ) |
44 |
|
xpss12 |
|- ( ( x C_ X /\ y C_ Y ) -> ( x X. y ) C_ ( X X. Y ) ) |
45 |
41 43 44
|
syl2an |
|- ( ( x e. R /\ y e. S ) -> ( x X. y ) C_ ( X X. Y ) ) |
46 |
|
vex |
|- x e. _V |
47 |
|
vex |
|- y e. _V |
48 |
46 47
|
xpex |
|- ( x X. y ) e. _V |
49 |
48
|
elpw |
|- ( ( x X. y ) e. ~P ( X X. Y ) <-> ( x X. y ) C_ ( X X. Y ) ) |
50 |
45 49
|
sylibr |
|- ( ( x e. R /\ y e. S ) -> ( x X. y ) e. ~P ( X X. Y ) ) |
51 |
50
|
rgen2 |
|- A. x e. R A. y e. S ( x X. y ) e. ~P ( X X. Y ) |
52 |
28
|
fmpo |
|- ( A. x e. R A. y e. S ( x X. y ) e. ~P ( X X. Y ) <-> ( x e. R , y e. S |-> ( x X. y ) ) : ( R X. S ) --> ~P ( X X. Y ) ) |
53 |
51 52
|
mpbi |
|- ( x e. R , y e. S |-> ( x X. y ) ) : ( R X. S ) --> ~P ( X X. Y ) |
54 |
|
frn |
|- ( ( x e. R , y e. S |-> ( x X. y ) ) : ( R X. S ) --> ~P ( X X. Y ) -> ran ( x e. R , y e. S |-> ( x X. y ) ) C_ ~P ( X X. Y ) ) |
55 |
53 54
|
ax-mp |
|- ran ( x e. R , y e. S |-> ( x X. y ) ) C_ ~P ( X X. Y ) |
56 |
1 55
|
eqsstri |
|- B C_ ~P ( X X. Y ) |
57 |
|
sspwuni |
|- ( B C_ ~P ( X X. Y ) <-> U. B C_ ( X X. Y ) ) |
58 |
56 57
|
mpbi |
|- U. B C_ ( X X. Y ) |
59 |
39 58
|
eqssi |
|- ( X X. Y ) = U. B |