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	biimtrrid	|- ( ( 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