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

Metamath Proof Explorer

Theorem txuni2

Proof