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 syl5bir ( ( 𝑟𝑅𝑠𝑆 ) → ( ( 𝑧𝑟𝑤𝑠 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐵 ) )
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 ( 𝑋 × 𝑌 ) = 𝐵