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 \in R, y \in S ⟼ x \times y)$
	txuni2.1	$⊢ X = ⋃ R$
	txuni2.2	$⊢ Y = ⋃ S$
Assertion	txuni2	$⊢ X \times Y = ⋃ B$

Proof

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

Metamath Proof Explorer

Theorem txuni2

Proof