Theorem txuni2

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

	Ref	Expression
Hypotheses	txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
	txuni2.1	⊢ 𝑋 = ∪ 𝑅
	txuni2.2	⊢ 𝑌 = ∪ 𝑆
Assertion	txuni2	⊢ ( 𝑋 × 𝑌 ) = ∪ 𝐵

Proof

Step	Hyp	Ref	Expression
1		txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
2		txuni2.1	⊢ 𝑋 = ∪ 𝑅
3		txuni2.2	⊢ 𝑌 = ∪ 𝑆
4		relxp	⊢ Rel ( 𝑋 × 𝑌 )
5	2	eleq2i	⊢ ( 𝑧 ∈ 𝑋 ↔ 𝑧 ∈ ∪ 𝑅 )
6		eluni2	⊢ ( 𝑧 ∈ ∪ 𝑅 ↔ ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 )
7	5 6	bitri	⊢ ( 𝑧 ∈ 𝑋 ↔ ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 )
8	3	eleq2i	⊢ ( 𝑤 ∈ 𝑌 ↔ 𝑤 ∈ ∪ 𝑆 )
9		eluni2	⊢ ( 𝑤 ∈ ∪ 𝑆 ↔ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 )
10	8 9	bitri	⊢ ( 𝑤 ∈ 𝑌 ↔ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 )
11	7 10	anbi12i	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ∧ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) )
12		opelxp	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) )
13		reeanv	⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ∧ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) )
14	11 12 13	3bitr4i	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) )
15		opelxp	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑟 × 𝑠 ) ↔ ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) )
16		eqid	⊢ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 )
17		xpeq1	⊢ ( 𝑥 = 𝑟 → ( 𝑥 × 𝑦 ) = ( 𝑟 × 𝑦 ) )
18	17	eqeq2d	⊢ ( 𝑥 = 𝑟 → ( ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑦 ) ) )
19		xpeq2	⊢ ( 𝑦 = 𝑠 → ( 𝑟 × 𝑦 ) = ( 𝑟 × 𝑠 ) )
20	19	eqeq2d	⊢ ( 𝑦 = 𝑠 → ( ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 ) ) )
21	18 20	rspc2ev	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) )
22	16 21	mp3an3	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) )
23		vex	⊢ 𝑟 ∈ V
24		vex	⊢ 𝑠 ∈ V
25	23 24	xpex	⊢ ( 𝑟 × 𝑠 ) ∈ V
26		eqeq1	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( 𝑧 = ( 𝑥 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) )
27	26	2rexbidv	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) )
28		eqid	⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
29	28	rnmpo	⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) }
30	1 29	eqtri	⊢ 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) }
31	25 27 30	elab2	⊢ ( ( 𝑟 × 𝑠 ) ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) )
32	22 31	sylibr	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑟 × 𝑠 ) ∈ 𝐵 )
33		elssuni	⊢ ( ( 𝑟 × 𝑠 ) ∈ 𝐵 → ( 𝑟 × 𝑠 ) ⊆ ∪ 𝐵 )
34	32 33	syl	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑟 × 𝑠 ) ⊆ ∪ 𝐵 )
35	34	sseld	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑟 × 𝑠 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ 𝐵 ) )
36	15 35	biimtrrid	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ 𝐵 ) )
37	36	rexlimivv	⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ 𝐵 )
38	14 37	sylbi	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑋 × 𝑌 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ 𝐵 )
39	4 38	relssi	⊢ ( 𝑋 × 𝑌 ) ⊆ ∪ 𝐵
40		elssuni	⊢ ( 𝑥 ∈ 𝑅 → 𝑥 ⊆ ∪ 𝑅 )
41	40 2	sseqtrrdi	⊢ ( 𝑥 ∈ 𝑅 → 𝑥 ⊆ 𝑋 )
42		elssuni	⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ ∪ 𝑆 )
43	42 3	sseqtrrdi	⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ 𝑌 )
44		xpss12	⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
45	41 43 44	syl2an	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
46		vex	⊢ 𝑥 ∈ V
47		vex	⊢ 𝑦 ∈ V
48	46 47	xpex	⊢ ( 𝑥 × 𝑦 ) ∈ V
49	48	elpw	⊢ ( ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) ↔ ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
50	45 49	sylibr	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) )
51	50	rgen2	⊢ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 )
52	28	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) ↔ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 ) )
53	51 52	mpbi	⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 )
54		frn	⊢ ( ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 ) → ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( 𝑋 × 𝑌 ) )
55	53 54	ax-mp	⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( 𝑋 × 𝑌 )
56	1 55	eqsstri	⊢ 𝐵 ⊆ 𝒫 ( 𝑋 × 𝑌 )
57		sspwuni	⊢ ( 𝐵 ⊆ 𝒫 ( 𝑋 × 𝑌 ) ↔ ∪ 𝐵 ⊆ ( 𝑋 × 𝑌 ) )
58	56 57	mpbi	⊢ ∪ 𝐵 ⊆ ( 𝑋 × 𝑌 )
59	39 58	eqssi	⊢ ( 𝑋 × 𝑌 ) = ∪ 𝐵