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

Theorem xpstopnlem1 22136
 Description: The function 𝐹 used in xpsvalcda 16711 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 21918 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
41, 2, 3syl2anc 576 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
5 eqid 2771 . . . . . . . . . . . . 13 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
6 0ex 5064 . . . . . . . . . . . . . 14 ∅ ∈ V
76a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∅ ∈ V)
85, 7, 1pt1hmeo 22133 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})))
9 hmeocn 22087 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})) → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})))
10 cntop2 21568 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})) → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
118, 9, 103syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
12 toptopon2 21245 . . . . . . . . . . 11 ((∏t‘{⟨∅, 𝐽⟩}) ∈ Top ↔ (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
1311, 12sylib 210 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
14 eqid 2771 . . . . . . . . . . . . 13 (∏t‘{⟨1o, 𝐾⟩}) = (∏t‘{⟨1o, 𝐾⟩})
15 1on 7910 . . . . . . . . . . . . . 14 1o ∈ On
1615a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1o ∈ On)
1714, 16, 2pt1hmeo 22133 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})))
18 hmeocn 22087 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})) → (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})))
19 cntop2 21568 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})) → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
2017, 18, 193syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
21 toptopon2 21245 . . . . . . . . . . 11 ((∏t‘{⟨1o, 𝐾⟩}) ∈ Top ↔ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩})))
2220, 21sylib 210 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩})))
23 txtopon 21918 . . . . . . . . . 10 (((∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})) ∧ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩}))) → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))))
2413, 22, 23syl2anc 576 . . . . . . . . 9 (𝜑 → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))))
25 opeq2 4674 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑥⟩)
2625sneqd 4447 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → {⟨∅, 𝑧⟩} = {⟨∅, 𝑥⟩})
27 eqid 2771 . . . . . . . . . . . . . . 15 (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) = (𝑧𝑋 ↦ {⟨∅, 𝑧⟩})
28 snex 5184 . . . . . . . . . . . . . . 15 {⟨∅, 𝑥⟩} ∈ V
2926, 27, 28fvmpt 6593 . . . . . . . . . . . . . 14 (𝑥𝑋 → ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩})
30 opeq2 4674 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ⟨1o, 𝑧⟩ = ⟨1o, 𝑦⟩)
3130sneqd 4447 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → {⟨1o, 𝑧⟩} = {⟨1o, 𝑦⟩})
32 eqid 2771 . . . . . . . . . . . . . . 15 (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) = (𝑧𝑌 ↦ {⟨1o, 𝑧⟩})
33 snex 5184 . . . . . . . . . . . . . . 15 {⟨1o, 𝑦⟩} ∈ V
3431, 32, 33fvmpt 6593 . . . . . . . . . . . . . 14 (𝑦𝑌 → ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩})
35 opeq12 4675 . . . . . . . . . . . . . 14 ((((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩} ∧ ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩}) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
3629, 34, 35syl2an 587 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑌) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
3736mpoeq3ia 7048 . . . . . . . . . . . 12 (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
38 toponuni 21241 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
391, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 = 𝐽)
40 toponuni 21241 . . . . . . . . . . . . . 14 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
412, 40syl 17 . . . . . . . . . . . . 13 (𝜑𝑌 = 𝐾)
42 mpoeq12 7043 . . . . . . . . . . . . 13 ((𝑋 = 𝐽𝑌 = 𝐾) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
4339, 41, 42syl2anc 576 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
4437, 43syl5eqr 2821 . . . . . . . . . . 11 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
45 eqid 2771 . . . . . . . . . . . 12 𝐽 = 𝐽
46 eqid 2771 . . . . . . . . . . . 12 𝐾 = 𝐾
4745, 46, 8, 17txhmeo 22130 . . . . . . . . . . 11 (𝜑 → (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
4844, 47eqeltrd 2859 . . . . . . . . . 10 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
49 hmeocn 22087 . . . . . . . . . 10 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
51 cnf2 21576 . . . . . . . . 9 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
524, 24, 50, 51syl3anc 1352 . . . . . . . 8 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
53 eqid 2771 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
5453fmpo 7572 . . . . . . . 8 (∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↔ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5552, 54sylibr 226 . . . . . . 7 (𝜑 → ∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5655r19.21bi 3151 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5756r19.21bi 3151 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑦𝑌) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5857anasss 459 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
59 eqidd 2772 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩))
60 vex 3411 . . . . . . . . 9 𝑥 ∈ V
61 vex 3411 . . . . . . . . 9 𝑦 ∈ V
6260, 61op1std 7509 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
6360, 61op2ndd 7510 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
6462, 63uneq12d 4022 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
6564mpompt 7080 . . . . . 6 (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦))
6665eqcomi 2780 . . . . 5 (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧)))
6766a1i 11 . . . 4 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))))
6828, 33op1std 7509 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (1st𝑧) = {⟨∅, 𝑥⟩})
6928, 33op2ndd 7510 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (2nd𝑧) = {⟨1o, 𝑦⟩})
7068, 69uneq12d 4022 . . . . 5 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩}))
71 xpscg 16685 . . . . . . 7 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
7271el2v 3415 . . . . . 6 ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
73 df-pr 4438 . . . . . 6 {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩})
7472, 73eqtri 2795 . . . . 5 ({𝑥} +𝑐 {𝑦}) = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩})
7570, 74syl6eqr 2825 . . . 4 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({𝑥} +𝑐 {𝑦}))
7658, 59, 67, 75fmpoco 7596 . . 3 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
77 xpstopnlem1.f . . 3 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
7876, 77syl6reqr 2826 . 2 (𝜑𝐹 = ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)))
79 eqid 2771 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
80 eqid 2771 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o}))
81 eqid 2771 . . . . 5 (∏t({𝐽} +𝑐 {𝐾})) = (∏t({𝐽} +𝑐 {𝐾}))
82 eqid 2771 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
83 eqid 2771 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o}))
84 eqid 2771 . . . . 5 (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥𝑦))
85 2on 7912 . . . . . 6 2o ∈ On
8685a1i 11 . . . . 5 (𝜑 → 2o ∈ On)
87 topontop 21240 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
881, 87syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
89 topontop 21240 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
902, 89syl 17 . . . . . 6 (𝜑𝐾 ∈ Top)
91 xpscfcda 16699 . . . . . 6 (({𝐽} +𝑐 {𝐾}):2o⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
9288, 90, 91sylanbrc 575 . . . . 5 (𝜑({𝐽} +𝑐 {𝐾}):2o⟶Top)
93 df2o3 7917 . . . . . . 7 2o = {∅, 1o}
94 df-pr 4438 . . . . . . 7 {∅, 1o} = ({∅} ∪ {1o})
9593, 94eqtri 2795 . . . . . 6 2o = ({∅} ∪ {1o})
9695a1i 11 . . . . 5 (𝜑 → 2o = ({∅} ∪ {1o}))
97 1n0 7919 . . . . . . 7 1o ≠ ∅
9897necomi 3014 . . . . . 6 ∅ ≠ 1o
99 disjsn2 4518 . . . . . 6 (∅ ≠ 1o → ({∅} ∩ {1o}) = ∅)
10098, 99mp1i 13 . . . . 5 (𝜑 → ({∅} ∩ {1o}) = ∅)
10179, 80, 81, 82, 83, 84, 86, 92, 96, 100ptunhmeo 22135 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥𝑦)) ∈ (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
102 xpscfn 16686 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ({𝐽} +𝑐 {𝐾}) Fn 2o)
1031, 2, 102syl2anc 576 . . . . . . . . 9 (𝜑({𝐽} +𝑐 {𝐾}) Fn 2o)
1046prid1 4568 . . . . . . . . . 10 ∅ ∈ {∅, 1o}
105104, 93eleqtrri 2858 . . . . . . . . 9 ∅ ∈ 2o
106 fnressn 6741 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2o ∧ ∅ ∈ 2o) → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
107103, 105, 106sylancl 578 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
108 xpsc0 16689 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
1091, 108syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
110109opeq2d 4680 . . . . . . . . 9 (𝜑 → ⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩ = ⟨∅, 𝐽⟩)
111110sneqd 4447 . . . . . . . 8 (𝜑 → {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩} = {⟨∅, 𝐽⟩})
112107, 111eqtrd 2807 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, 𝐽⟩})
113112fveq2d 6500 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
114113unieqd 4718 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
115 1oex 7911 . . . . . . . . . . 11 1o ∈ V
116115prid2 4569 . . . . . . . . . 10 1o ∈ {∅, 1o}
117116, 93eleqtrri 2858 . . . . . . . . 9 1o ∈ 2o
118 fnressn 6741 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2o ∧ 1o ∈ 2o) → (({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, (({𝐽} +𝑐 {𝐾})‘1o)⟩})
119103, 117, 118sylancl 578 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, (({𝐽} +𝑐 {𝐾})‘1o)⟩})
120 xpsc1 16690 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → (({𝐽} +𝑐 {𝐾})‘1o) = 𝐾)
1212, 120syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘1o) = 𝐾)
122121opeq2d 4680 . . . . . . . . 9 (𝜑 → ⟨1o, (({𝐽} +𝑐 {𝐾})‘1o)⟩ = ⟨1o, 𝐾⟩)
123122sneqd 4447 . . . . . . . 8 (𝜑 → {⟨1o, (({𝐽} +𝑐 {𝐾})‘1o)⟩} = {⟨1o, 𝐾⟩})
124119, 123eqtrd 2807 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, 𝐾⟩})
125124fveq2d 6500 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘{⟨1o, 𝐾⟩}))
126125unieqd 4718 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘{⟨1o, 𝐾⟩}))
127 eqidd 2772 . . . . 5 (𝜑 → (𝑥𝑦) = (𝑥𝑦))
128114, 126, 127mpoeq123dv 7045 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)))
129113, 125oveq12d 6992 . . . . 5 (𝜑 → ((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o}))) = ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))
130129oveq1d 6989 . . . 4 (𝜑 → (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1o})))Homeo(∏t({𝐽} +𝑐 {𝐾}))) = (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
131101, 128, 1303eltr3d 2873 . . 3 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
132 hmeoco 22099 . . 3 (((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾})))) → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
13348, 131, 132syl2anc 576 . 2 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
13478, 133eqeltrd 2859 1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ∈ wcel 2051   ≠ wne 2960  ∀wral 3081  Vcvv 3408   ∪ cun 3820   ∩ cin 3821  ∅c0 4172  {csn 4435  {cpr 4437  ⟨cop 4441  ∪ cuni 4708   ↦ cmpt 5004   × cxp 5401  ◡ccnv 5402   ↾ cres 5405   ∘ ccom 5407  Oncon0 6026   Fn wfn 6180  ⟶wf 6181  ‘cfv 6185  (class class class)co 6974   ∈ cmpo 6976  1st c1st 7497  2nd c2nd 7498  1oc1o 7896  2oc2o 7897   +𝑐 ccda 9385  ∏tcpt 16566  Topctop 21220  TopOnctopon 21237   Cn ccn 21551   ×t ctx 21887  Homeochmeo 22080 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-iin 4791  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-2o 7904  df-oadd 7907  df-er 8087  df-map 8206  df-ixp 8258  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-fi 8668  df-cda 9386  df-topgen 16571  df-pt 16572  df-top 21221  df-topon 21238  df-bases 21273  df-cn 21554  df-cnp 21555  df-tx 21889  df-hmeo 22082 This theorem is referenced by:  xpstopnlem2  22138
 Copyright terms: Public domain W3C validator