Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpstopnlem1 Structured version   Visualization version   GIF version

Theorem xpstopnlem1 21525
 Description: The function 𝐹 used in xpsval 16156 is a homeomorphism from the binary product topology to the indexed product topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
xpstopnlem1.f 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
xpstopnlem1.j (𝜑𝐽 ∈ (TopOn‘𝑋))
xpstopnlem1.k (𝜑𝐾 ∈ (TopOn‘𝑌))
Assertion
Ref Expression
xpstopnlem1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem xpstopnlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 xpstopnlem1.j . . . . . . . . . 10 (𝜑𝐽 ∈ (TopOn‘𝑋))
2 xpstopnlem1.k . . . . . . . . . 10 (𝜑𝐾 ∈ (TopOn‘𝑌))
3 txtopon 21307 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
41, 2, 3syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
5 eqid 2621 . . . . . . . . . . . . 13 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
6 0ex 4752 . . . . . . . . . . . . . 14 ∅ ∈ V
76a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∅ ∈ V)
85, 7, 1pt1hmeo 21522 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})))
9 hmeocn 21476 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})) → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})))
10 cntop2 20958 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})) → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
118, 9, 103syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
12 eqid 2621 . . . . . . . . . . . 12 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
1312toptopon 20647 . . . . . . . . . . 11 ((∏t‘{⟨∅, 𝐽⟩}) ∈ Top ↔ (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
1411, 13sylib 208 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
15 eqid 2621 . . . . . . . . . . . . 13 (∏t‘{⟨1𝑜, 𝐾⟩}) = (∏t‘{⟨1𝑜, 𝐾⟩})
16 1on 7515 . . . . . . . . . . . . . 14 1𝑜 ∈ On
1716a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1𝑜 ∈ On)
1815, 17, 2pt1hmeo 21522 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1𝑜, 𝐾⟩})))
19 hmeocn 21476 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1𝑜, 𝐾⟩})) → (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1𝑜, 𝐾⟩})))
20 cntop2 20958 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1𝑜, 𝐾⟩})) → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top)
2118, 19, 203syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top)
22 eqid 2621 . . . . . . . . . . . 12 (∏t‘{⟨1𝑜, 𝐾⟩}) = (∏t‘{⟨1𝑜, 𝐾⟩})
2322toptopon 20647 . . . . . . . . . . 11 ((∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top ↔ (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩})))
2421, 23sylib 208 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩})))
25 txtopon 21307 . . . . . . . . . 10 (((∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})) ∧ (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩}))) → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩}))))
2614, 24, 25syl2anc 692 . . . . . . . . 9 (𝜑 → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩}))))
27 opeq2 4373 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑥⟩)
2827sneqd 4162 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → {⟨∅, 𝑧⟩} = {⟨∅, 𝑥⟩})
29 eqid 2621 . . . . . . . . . . . . . . 15 (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) = (𝑧𝑋 ↦ {⟨∅, 𝑧⟩})
30 snex 4871 . . . . . . . . . . . . . . 15 {⟨∅, 𝑥⟩} ∈ V
3128, 29, 30fvmpt 6241 . . . . . . . . . . . . . 14 (𝑥𝑋 → ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩})
32 opeq2 4373 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ⟨1𝑜, 𝑧⟩ = ⟨1𝑜, 𝑦⟩)
3332sneqd 4162 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → {⟨1𝑜, 𝑧⟩} = {⟨1𝑜, 𝑦⟩})
34 eqid 2621 . . . . . . . . . . . . . . 15 (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) = (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})
35 snex 4871 . . . . . . . . . . . . . . 15 {⟨1𝑜, 𝑦⟩} ∈ V
3633, 34, 35fvmpt 6241 . . . . . . . . . . . . . 14 (𝑦𝑌 → ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦) = {⟨1𝑜, 𝑦⟩})
37 opeq12 4374 . . . . . . . . . . . . . 14 ((((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩} ∧ ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦) = {⟨1𝑜, 𝑦⟩}) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
3831, 36, 37syl2an 494 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑌) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
3938mpt2eq3ia 6676 . . . . . . . . . . . 12 (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
40 toponuni 20641 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
411, 40syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 = 𝐽)
42 toponuni 20641 . . . . . . . . . . . . . 14 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
432, 42syl 17 . . . . . . . . . . . . 13 (𝜑𝑌 = 𝐾)
44 mpt2eq12 6671 . . . . . . . . . . . . 13 ((𝑋 = 𝐽𝑌 = 𝐾) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
4541, 43, 44syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
4639, 45syl5eqr 2669 . . . . . . . . . . 11 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
47 eqid 2621 . . . . . . . . . . . 12 𝐽 = 𝐽
48 eqid 2621 . . . . . . . . . . . 12 𝐾 = 𝐾
4947, 48, 8, 18txhmeo 21519 . . . . . . . . . . 11 (𝜑 → (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
5046, 49eqeltrd 2698 . . . . . . . . . 10 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
51 hmeocn 21476 . . . . . . . . . 10 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
5250, 51syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
53 cnf2 20966 . . . . . . . . 9 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩}))) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
544, 26, 52, 53syl3anc 1323 . . . . . . . 8 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
55 eqid 2621 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
5655fmpt2 7185 . . . . . . . 8 (∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↔ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5754, 56sylibr 224 . . . . . . 7 (𝜑 → ∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5857r19.21bi 2927 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5958r19.21bi 2927 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑦𝑌) → ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
6059anasss 678 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
61 eqidd 2622 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩))
62 vex 3189 . . . . . . . . 9 𝑥 ∈ V
63 vex 3189 . . . . . . . . 9 𝑦 ∈ V
6462, 63op1std 7126 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
6562, 63op2ndd 7127 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
6664, 65uneq12d 3748 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
6766mpt2mpt 6708 . . . . . 6 (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦))
6867eqcomi 2630 . . . . 5 (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧)))
6968a1i 11 . . . 4 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))))
7030, 35op1std 7126 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → (1st𝑧) = {⟨∅, 𝑥⟩})
7130, 35op2ndd 7127 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → (2nd𝑧) = {⟨1𝑜, 𝑦⟩})
7270, 71uneq12d 3748 . . . . 5 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩}))
73 xpscg 16142 . . . . . . 7 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩})
7462, 63, 73mp2an 707 . . . . . 6 ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩}
75 df-pr 4153 . . . . . 6 {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩})
7674, 75eqtri 2643 . . . . 5 ({𝑥} +𝑐 {𝑦}) = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩})
7772, 76syl6eqr 2673 . . . 4 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({𝑥} +𝑐 {𝑦}))
7860, 61, 69, 77fmpt2co 7208 . . 3 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
79 xpstopnlem1.f . . 3 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
8078, 79syl6reqr 2674 . 2 (𝜑𝐹 = ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)))
81 eqid 2621 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
82 eqid 2621 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))
83 eqid 2621 . . . . 5 (∏t({𝐽} +𝑐 {𝐾})) = (∏t({𝐽} +𝑐 {𝐾}))
84 eqid 2621 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
85 eqid 2621 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))
86 eqid 2621 . . . . 5 (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦))
87 2on 7516 . . . . . 6 2𝑜 ∈ On
8887a1i 11 . . . . 5 (𝜑 → 2𝑜 ∈ On)
89 topontop 20640 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
901, 89syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
91 topontop 20640 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
922, 91syl 17 . . . . . 6 (𝜑𝐾 ∈ Top)
93 xpscf 16150 . . . . . 6 (({𝐽} +𝑐 {𝐾}):2𝑜⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
9490, 92, 93sylanbrc 697 . . . . 5 (𝜑({𝐽} +𝑐 {𝐾}):2𝑜⟶Top)
95 df2o3 7521 . . . . . . 7 2𝑜 = {∅, 1𝑜}
96 df-pr 4153 . . . . . . 7 {∅, 1𝑜} = ({∅} ∪ {1𝑜})
9795, 96eqtri 2643 . . . . . 6 2𝑜 = ({∅} ∪ {1𝑜})
9897a1i 11 . . . . 5 (𝜑 → 2𝑜 = ({∅} ∪ {1𝑜}))
99 1n0 7523 . . . . . . 7 1𝑜 ≠ ∅
10099necomi 2844 . . . . . 6 ∅ ≠ 1𝑜
101 disjsn2 4219 . . . . . 6 (∅ ≠ 1𝑜 → ({∅} ∩ {1𝑜}) = ∅)
102100, 101mp1i 13 . . . . 5 (𝜑 → ({∅} ∩ {1𝑜}) = ∅)
10381, 82, 83, 84, 85, 86, 88, 94, 98, 102ptunhmeo 21524 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) ∈ (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
104 xpscfn 16143 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ({𝐽} +𝑐 {𝐾}) Fn 2𝑜)
1051, 2, 104syl2anc 692 . . . . . . . . 9 (𝜑({𝐽} +𝑐 {𝐾}) Fn 2𝑜)
1066prid1 4269 . . . . . . . . . 10 ∅ ∈ {∅, 1𝑜}
107106, 95eleqtrri 2697 . . . . . . . . 9 ∅ ∈ 2𝑜
108 fnressn 6382 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧ ∅ ∈ 2𝑜) → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
109105, 107, 108sylancl 693 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
110 xpsc0 16144 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
1111, 110syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
112111opeq2d 4379 . . . . . . . . 9 (𝜑 → ⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩ = ⟨∅, 𝐽⟩)
113112sneqd 4162 . . . . . . . 8 (𝜑 → {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩} = {⟨∅, 𝐽⟩})
114109, 113eqtrd 2655 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, 𝐽⟩})
115114fveq2d 6154 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
116115unieqd 4414 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
11716elexi 3199 . . . . . . . . . . 11 1𝑜 ∈ V
118117prid2 4270 . . . . . . . . . 10 1𝑜 ∈ {∅, 1𝑜}
119118, 95eleqtrri 2697 . . . . . . . . 9 1𝑜 ∈ 2𝑜
120 fnressn 6382 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧ 1𝑜 ∈ 2𝑜) → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩})
121105, 119, 120sylancl 693 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩})
122 xpsc1 16145 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → (({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾)
1232, 122syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾)
124123opeq2d 4379 . . . . . . . . 9 (𝜑 → ⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩ = ⟨1𝑜, 𝐾⟩)
125124sneqd 4162 . . . . . . . 8 (𝜑 → {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩} = {⟨1𝑜, 𝐾⟩})
126121, 125eqtrd 2655 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, 𝐾⟩})
127126fveq2d 6154 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘{⟨1𝑜, 𝐾⟩}))
128127unieqd 4414 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘{⟨1𝑜, 𝐾⟩}))
129 eqidd 2622 . . . . 5 (𝜑 → (𝑥𝑦) = (𝑥𝑦))
130116, 128, 129mpt2eq123dv 6673 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)))
131115, 127oveq12d 6625 . . . . 5 (𝜑 → ((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))) = ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})))
132131oveq1d 6622 . . . 4 (𝜑 → (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})))Homeo(∏t({𝐽} +𝑐 {𝐾}))) = (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
133103, 130, 1323eltr3d 2712 . . 3 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
134 hmeoco 21488 . . 3 (((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))) ∧ (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾})))) → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
13550, 133, 134syl2anc 692 . 2 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
13680, 135eqeltrd 2698 1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  Vcvv 3186   ∪ cun 3554   ∩ cin 3555  ∅c0 3893  {csn 4150  {cpr 4152  ⟨cop 4156  ∪ cuni 4404   ↦ cmpt 4675   × cxp 5074  ◡ccnv 5075   ↾ cres 5078   ∘ ccom 5080  Oncon0 5684   Fn wfn 5844  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  1st c1st 7114  2nd c2nd 7115  1𝑜c1o 7501  2𝑜c2o 7502   +𝑐 ccda 8936  ∏tcpt 16023  Topctop 20620  TopOnctopon 20637   Cn ccn 20941   ×t ctx 21276  Homeochmeo 21469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-map 7807  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fi 8264  df-cda 8937  df-topgen 16028  df-pt 16029  df-top 20621  df-topon 20638  df-bases 20664  df-cn 20944  df-cnp 20945  df-tx 21278  df-hmeo 21471 This theorem is referenced by:  xpstopnlem2  21527
 Copyright terms: Public domain W3C validator