Metamath Proof Explorer


Theorem txuni2

Description: The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses txval.1
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )
txuni2.1
|- X = U. R
txuni2.2
|- Y = U. S
Assertion txuni2
|- ( X X. Y ) = U. B

Proof

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