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

Theorem xpstopnlem1 21826
Description: The function 𝐹 used in xpsval 16437 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 21608 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
41, 2, 3syl2anc 575 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
5 eqid 2806 . . . . . . . . . . . . 13 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
6 0ex 4984 . . . . . . . . . . . . . 14 ∅ ∈ V
76a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∅ ∈ V)
85, 7, 1pt1hmeo 21823 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})))
9 hmeocn 21777 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})) → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})))
10 cntop2 21259 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})) → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
118, 9, 103syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
12 eqid 2806 . . . . . . . . . . . 12 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
1312toptopon 20935 . . . . . . . . . . 11 ((∏t‘{⟨∅, 𝐽⟩}) ∈ Top ↔ (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
1411, 13sylib 209 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
15 eqid 2806 . . . . . . . . . . . . 13 (∏t‘{⟨1𝑜, 𝐾⟩}) = (∏t‘{⟨1𝑜, 𝐾⟩})
16 1on 7803 . . . . . . . . . . . . . 14 1𝑜 ∈ On
1716a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1𝑜 ∈ On)
1815, 17, 2pt1hmeo 21823 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1𝑜, 𝐾⟩})))
19 hmeocn 21777 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1𝑜, 𝐾⟩})) → (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1𝑜, 𝐾⟩})))
20 cntop2 21259 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1𝑜, 𝐾⟩})) → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top)
2118, 19, 203syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top)
22 eqid 2806 . . . . . . . . . . . 12 (∏t‘{⟨1𝑜, 𝐾⟩}) = (∏t‘{⟨1𝑜, 𝐾⟩})
2322toptopon 20935 . . . . . . . . . . 11 ((∏t‘{⟨1𝑜, 𝐾⟩}) ∈ Top ↔ (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩})))
2421, 23sylib 209 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩})))
25 txtopon 21608 . . . . . . . . . 10 (((∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})) ∧ (∏t‘{⟨1𝑜, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1𝑜, 𝐾⟩}))) → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩}))))
2614, 24, 25syl2anc 575 . . . . . . . . 9 (𝜑 → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩}))))
27 opeq2 4596 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑥⟩)
2827sneqd 4382 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → {⟨∅, 𝑧⟩} = {⟨∅, 𝑥⟩})
29 eqid 2806 . . . . . . . . . . . . . . 15 (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) = (𝑧𝑋 ↦ {⟨∅, 𝑧⟩})
30 snex 5098 . . . . . . . . . . . . . . 15 {⟨∅, 𝑥⟩} ∈ V
3128, 29, 30fvmpt 6503 . . . . . . . . . . . . . 14 (𝑥𝑋 → ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩})
32 opeq2 4596 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ⟨1𝑜, 𝑧⟩ = ⟨1𝑜, 𝑦⟩)
3332sneqd 4382 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → {⟨1𝑜, 𝑧⟩} = {⟨1𝑜, 𝑦⟩})
34 eqid 2806 . . . . . . . . . . . . . . 15 (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩}) = (𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})
35 snex 5098 . . . . . . . . . . . . . . 15 {⟨1𝑜, 𝑦⟩} ∈ V
3633, 34, 35fvmpt 6503 . . . . . . . . . . . . . 14 (𝑦𝑌 → ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦) = {⟨1𝑜, 𝑦⟩})
37 opeq12 4597 . . . . . . . . . . . . . 14 ((((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩} ∧ ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦) = {⟨1𝑜, 𝑦⟩}) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
3831, 36, 37syl2an 585 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑌) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
3938mpt2eq3ia 6950 . . . . . . . . . . . 12 (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
40 toponuni 20932 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
411, 40syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 = 𝐽)
42 toponuni 20932 . . . . . . . . . . . . . 14 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
432, 42syl 17 . . . . . . . . . . . . 13 (𝜑𝑌 = 𝐾)
44 mpt2eq12 6945 . . . . . . . . . . . . 13 ((𝑋 = 𝐽𝑌 = 𝐾) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
4541, 43, 44syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
4639, 45syl5eqr 2854 . . . . . . . . . . 11 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩))
47 eqid 2806 . . . . . . . . . . . 12 𝐽 = 𝐽
48 eqid 2806 . . . . . . . . . . . 12 𝐾 = 𝐾
4947, 48, 8, 18txhmeo 21820 . . . . . . . . . . 11 (𝜑 → (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1𝑜, 𝑧⟩})‘𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
5046, 49eqeltrd 2885 . . . . . . . . . 10 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))))
51 hmeocn 21777 . . . . . . . . . 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 21267 . . . . . . . . 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 1483 . . . . . . . 8 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
55 eqid 2806 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)
5655fmpt2 7470 . . . . . . . 8 (∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↔ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5754, 56sylibr 225 . . . . . . 7 (𝜑 → ∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5857r19.21bi 3120 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
5958r19.21bi 3120 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑦𝑌) → ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
6059anasss 454 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})))
61 eqidd 2807 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩))
62 vex 3394 . . . . . . . . 9 𝑥 ∈ V
63 vex 3394 . . . . . . . . 9 𝑦 ∈ V
6462, 63op1std 7408 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
6562, 63op2ndd 7409 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
6664, 65uneq12d 3967 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
6766mpt2mpt 6982 . . . . . 6 (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦))
6867eqcomi 2815 . . . . 5 (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧)))
6968a1i 11 . . . 4 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1𝑜, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))))
7030, 35op1std 7408 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → (1st𝑧) = {⟨∅, 𝑥⟩})
7130, 35op2ndd 7409 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → (2nd𝑧) = {⟨1𝑜, 𝑦⟩})
7270, 71uneq12d 3967 . . . . 5 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩}))
73 xpscg 16423 . . . . . . 7 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩})
7462, 63, 73mp2an 675 . . . . . 6 ({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩}
75 df-pr 4373 . . . . . 6 {⟨∅, 𝑥⟩, ⟨1𝑜, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩})
7674, 75eqtri 2828 . . . . 5 ({𝑥} +𝑐 {𝑦}) = ({⟨∅, 𝑥⟩} ∪ {⟨1𝑜, 𝑦⟩})
7772, 76syl6eqr 2858 . . . 4 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({𝑥} +𝑐 {𝑦}))
7860, 61, 69, 77fmpt2co 7494 . . 3 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
79 xpstopnlem1.f . . 3 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
8078, 79syl6reqr 2859 . 2 (𝜑𝐹 = ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)))
81 eqid 2806 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
82 eqid 2806 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))
83 eqid 2806 . . . . 5 (∏t({𝐽} +𝑐 {𝐾})) = (∏t({𝐽} +𝑐 {𝐾}))
84 eqid 2806 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅}))
85 eqid 2806 . . . . 5 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))
86 eqid 2806 . . . . 5 (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦))
87 2on 7805 . . . . . 6 2𝑜 ∈ On
8887a1i 11 . . . . 5 (𝜑 → 2𝑜 ∈ On)
89 topontop 20931 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
901, 89syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
91 topontop 20931 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
922, 91syl 17 . . . . . 6 (𝜑𝐾 ∈ Top)
93 xpscf 16431 . . . . . 6 (({𝐽} +𝑐 {𝐾}):2𝑜⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
9490, 92, 93sylanbrc 574 . . . . 5 (𝜑({𝐽} +𝑐 {𝐾}):2𝑜⟶Top)
95 df2o3 7810 . . . . . . 7 2𝑜 = {∅, 1𝑜}
96 df-pr 4373 . . . . . . 7 {∅, 1𝑜} = ({∅} ∪ {1𝑜})
9795, 96eqtri 2828 . . . . . 6 2𝑜 = ({∅} ∪ {1𝑜})
9897a1i 11 . . . . 5 (𝜑 → 2𝑜 = ({∅} ∪ {1𝑜}))
99 1n0 7812 . . . . . . 7 1𝑜 ≠ ∅
10099necomi 3032 . . . . . 6 ∅ ≠ 1𝑜
101 disjsn2 4439 . . . . . 6 (∅ ≠ 1𝑜 → ({∅} ∩ {1𝑜}) = ∅)
102100, 101mp1i 13 . . . . 5 (𝜑 → ({∅} ∩ {1𝑜}) = ∅)
10381, 82, 83, 84, 85, 86, 88, 94, 98, 102ptunhmeo 21825 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) ∈ (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
104 xpscfn 16424 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ({𝐽} +𝑐 {𝐾}) Fn 2𝑜)
1051, 2, 104syl2anc 575 . . . . . . . . 9 (𝜑({𝐽} +𝑐 {𝐾}) Fn 2𝑜)
1066prid1 4488 . . . . . . . . . 10 ∅ ∈ {∅, 1𝑜}
107106, 95eleqtrri 2884 . . . . . . . . 9 ∅ ∈ 2𝑜
108 fnressn 6649 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧ ∅ ∈ 2𝑜) → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
109105, 107, 108sylancl 576 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩})
110 xpsc0 16425 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
1111, 110syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
112111opeq2d 4602 . . . . . . . . 9 (𝜑 → ⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩ = ⟨∅, 𝐽⟩)
113112sneqd 4382 . . . . . . . 8 (𝜑 → {⟨∅, (({𝐽} +𝑐 {𝐾})‘∅)⟩} = {⟨∅, 𝐽⟩})
114109, 113eqtrd 2840 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, 𝐽⟩})
115114fveq2d 6412 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
116115unieqd 4640 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
117 1oex 7804 . . . . . . . . . . 11 1𝑜 ∈ V
118117prid2 4489 . . . . . . . . . 10 1𝑜 ∈ {∅, 1𝑜}
119118, 95eleqtrri 2884 . . . . . . . . 9 1𝑜 ∈ 2𝑜
120 fnressn 6649 . . . . . . . . 9 ((({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧ 1𝑜 ∈ 2𝑜) → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩})
121105, 119, 120sylancl 576 . . . . . . . 8 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩})
122 xpsc1 16426 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → (({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾)
1232, 122syl 17 . . . . . . . . . 10 (𝜑 → (({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾)
124123opeq2d 4602 . . . . . . . . 9 (𝜑 → ⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩ = ⟨1𝑜, 𝐾⟩)
125124sneqd 4382 . . . . . . . 8 (𝜑 → {⟨1𝑜, (({𝐽} +𝑐 {𝐾})‘1𝑜)⟩} = {⟨1𝑜, 𝐾⟩})
126121, 125eqtrd 2840 . . . . . . 7 (𝜑 → (({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) = {⟨1𝑜, 𝐾⟩})
127126fveq2d 6412 . . . . . 6 (𝜑 → (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘{⟨1𝑜, 𝐾⟩}))
128127unieqd 4640 . . . . 5 (𝜑 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = (∏t‘{⟨1𝑜, 𝐾⟩}))
129 eqidd 2807 . . . . 5 (𝜑 → (𝑥𝑦) = (𝑥𝑦))
130116, 128, 129mpt2eq123dv 6947 . . . 4 (𝜑 → (𝑥 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)))
131115, 127oveq12d 6892 . . . . 5 (𝜑 → ((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))) = ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩})))
132131oveq1d 6889 . . . 4 (𝜑 → (((∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})))Homeo(∏t({𝐽} +𝑐 {𝐾}))) = (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
133103, 130, 1323eltr3d 2899 . . 3 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1𝑜, 𝐾⟩}))Homeo(∏t({𝐽} +𝑐 {𝐾}))))
134 hmeoco 21789 . . 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 575 . 2 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1𝑜, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1𝑜, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
13680, 135eqeltrd 2885 1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t({𝐽} +𝑐 {𝐾}))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  wne 2978  wral 3096  Vcvv 3391  cun 3767  cin 3768  c0 4116  {csn 4370  {cpr 4372  cop 4376   cuni 4630  cmpt 4923   × cxp 5309  ccnv 5310  cres 5313  ccom 5315  Oncon0 5936   Fn wfn 6096  wf 6097  cfv 6101  (class class class)co 6874  cmpt2 6876  1st c1st 7396  2nd c2nd 7397  1𝑜c1o 7789  2𝑜c2o 7790   +𝑐 ccda 9274  tcpt 16304  Topctop 20911  TopOnctopon 20928   Cn ccn 21242   ×t ctx 21577  Homeochmeo 21770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fi 8556  df-cda 9275  df-topgen 16309  df-pt 16310  df-top 20912  df-topon 20929  df-bases 20964  df-cn 21245  df-cnp 21246  df-tx 21579  df-hmeo 21772
This theorem is referenced by:  xpstopnlem2  21828
  Copyright terms: Public domain W3C validator