This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = 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 ⊢ ( 𝑋 × 𝑌 ) = ∪ 𝐵