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

Theorem xpstopnlem1 23801
Description: The function 𝐹 used in xpsval 17580 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 𝐹 = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
xpstopnlem1.j (𝜑𝐽 ∈ (TopOn‘𝑋))
xpstopnlem1.k (𝜑𝐾 ∈ (TopOn‘𝑌))
Assertion
Ref Expression
xpstopnlem1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem xpstopnlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 xpstopnlem1.f . . 3 𝐹 = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
2 xpstopnlem1.j . . . . . . . . . 10 (𝜑𝐽 ∈ (TopOn‘𝑋))
3 xpstopnlem1.k . . . . . . . . . 10 (𝜑𝐾 ∈ (TopOn‘𝑌))
4 txtopon 23583 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
52, 3, 4syl2anc 582 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
6 eqid 2726 . . . . . . . . . . . . 13 (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
7 0ex 5304 . . . . . . . . . . . . . 14 ∅ ∈ V
87a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∅ ∈ V)
96, 8, 2pt1hmeo 23798 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})))
10 hmeocn 23752 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})) → (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})))
11 cntop2 23233 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})) → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
129, 10, 113syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
13 toptopon2 22908 . . . . . . . . . . 11 ((∏t‘{⟨∅, 𝐽⟩}) ∈ Top ↔ (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
1412, 13sylib 217 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})))
15 eqid 2726 . . . . . . . . . . . . 13 (∏t‘{⟨1o, 𝐾⟩}) = (∏t‘{⟨1o, 𝐾⟩})
16 1on 8500 . . . . . . . . . . . . . 14 1o ∈ On
1716a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1o ∈ On)
1815, 17, 3pt1hmeo 23798 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})))
19 hmeocn 23752 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})) → (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})))
20 cntop2 23233 . . . . . . . . . . . 12 ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})) → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
2118, 19, 203syl 18 . . . . . . . . . . 11 (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
22 toptopon2 22908 . . . . . . . . . . 11 ((∏t‘{⟨1o, 𝐾⟩}) ∈ Top ↔ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩})))
2321, 22sylib 217 . . . . . . . . . 10 (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩})))
24 txtopon 23583 . . . . . . . . . 10 (((∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘ (∏t‘{⟨∅, 𝐽⟩})) ∧ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘ (∏t‘{⟨1o, 𝐾⟩}))) → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))))
2514, 23, 24syl2anc 582 . . . . . . . . 9 (𝜑 → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))))
26 opeq2 4872 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑥⟩)
2726sneqd 4635 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → {⟨∅, 𝑧⟩} = {⟨∅, 𝑥⟩})
28 eqid 2726 . . . . . . . . . . . . . . 15 (𝑧𝑋 ↦ {⟨∅, 𝑧⟩}) = (𝑧𝑋 ↦ {⟨∅, 𝑧⟩})
29 snex 5429 . . . . . . . . . . . . . . 15 {⟨∅, 𝑥⟩} ∈ V
3027, 28, 29fvmpt 7001 . . . . . . . . . . . . . 14 (𝑥𝑋 → ((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩})
31 opeq2 4872 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ⟨1o, 𝑧⟩ = ⟨1o, 𝑦⟩)
3231sneqd 4635 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → {⟨1o, 𝑧⟩} = {⟨1o, 𝑦⟩})
33 eqid 2726 . . . . . . . . . . . . . . 15 (𝑧𝑌 ↦ {⟨1o, 𝑧⟩}) = (𝑧𝑌 ↦ {⟨1o, 𝑧⟩})
34 snex 5429 . . . . . . . . . . . . . . 15 {⟨1o, 𝑦⟩} ∈ V
3532, 33, 34fvmpt 7001 . . . . . . . . . . . . . 14 (𝑦𝑌 → ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩})
36 opeq12 4873 . . . . . . . . . . . . . 14 ((((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩} ∧ ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩}) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
3730, 35, 36syl2an 594 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑌) → ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
3837mpoeq3ia 7495 . . . . . . . . . . . 12 (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
39 toponuni 22904 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
402, 39syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 = 𝐽)
41 toponuni 22904 . . . . . . . . . . . . . 14 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
423, 41syl 17 . . . . . . . . . . . . 13 (𝜑𝑌 = 𝐾)
43 mpoeq12 7490 . . . . . . . . . . . . 13 ((𝑋 = 𝐽𝑌 = 𝐾) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
4440, 42, 43syl2anc 582 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
4538, 44eqtr3id 2780 . . . . . . . . . . 11 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
46 eqid 2726 . . . . . . . . . . . 12 𝐽 = 𝐽
47 eqid 2726 . . . . . . . . . . . 12 𝐾 = 𝐾
4846, 47, 9, 18txhmeo 23795 . . . . . . . . . . 11 (𝜑 → (𝑥 𝐽, 𝑦 𝐾 ↦ ⟨((𝑧𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
4945, 48eqeltrd 2826 . . . . . . . . . 10 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
50 hmeocn 23752 . . . . . . . . . 10 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
5149, 50syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
52 cnf2 23241 . . . . . . . . 9 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))) → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
535, 25, 51, 52syl3anc 1368 . . . . . . . 8 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
54 eqid 2726 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
5554fmpo 8074 . . . . . . . 8 (∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↔ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5653, 55sylibr 233 . . . . . . 7 (𝜑 → ∀𝑥𝑋𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5756r19.21bi 3239 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5857r19.21bi 3239 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑦𝑌) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
5958anasss 465 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})))
60 eqidd 2727 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩))
61 vex 3466 . . . . . . . . 9 𝑥 ∈ V
62 vex 3466 . . . . . . . . 9 𝑦 ∈ V
6361, 62op1std 8005 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
6461, 62op2ndd 8006 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
6563, 64uneq12d 4161 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
6665mpompt 7531 . . . . . 6 (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦))
6766eqcomi 2735 . . . . 5 (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧)))
6867a1i 11 . . . 4 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) = (𝑧 ∈ ( (∏t‘{⟨∅, 𝐽⟩}) × (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st𝑧) ∪ (2nd𝑧))))
6929, 34op1std 8005 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (1st𝑧) = {⟨∅, 𝑥⟩})
7029, 34op2ndd 8006 . . . . . 6 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (2nd𝑧) = {⟨1o, 𝑦⟩})
7169, 70uneq12d 4161 . . . . 5 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩}))
72 df-pr 4626 . . . . 5 {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩})
7371, 72eqtr4di 2784 . . . 4 (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st𝑧) ∪ (2nd𝑧)) = {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
7459, 60, 68, 73fmpoco 8101 . . 3 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
751, 74eqtr4id 2785 . 2 (𝜑𝐹 = ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)))
76 eqid 2726 . . . . 5 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) = (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅}))
77 eqid 2726 . . . . 5 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) = (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}))
78 eqid 2726 . . . . 5 (∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}) = (∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})
79 eqid 2726 . . . . 5 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) = (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅}))
80 eqid 2726 . . . . 5 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) = (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}))
81 eqid 2726 . . . . 5 (𝑥 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})), 𝑦 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})), 𝑦 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) ↦ (𝑥𝑦))
82 2on 8502 . . . . . 6 2o ∈ On
8382a1i 11 . . . . 5 (𝜑 → 2o ∈ On)
84 topontop 22903 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
852, 84syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
86 topontop 22903 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
873, 86syl 17 . . . . . 6 (𝜑𝐾 ∈ Top)
88 xpscf 17575 . . . . . 6 ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}:2o⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
8985, 87, 88sylanbrc 581 . . . . 5 (𝜑 → {⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}:2o⟶Top)
90 df2o3 8496 . . . . . . 7 2o = {∅, 1o}
91 df-pr 4626 . . . . . . 7 {∅, 1o} = ({∅} ∪ {1o})
9290, 91eqtri 2754 . . . . . 6 2o = ({∅} ∪ {1o})
9392a1i 11 . . . . 5 (𝜑 → 2o = ({∅} ∪ {1o}))
94 1n0 8510 . . . . . . 7 1o ≠ ∅
9594necomi 2985 . . . . . 6 ∅ ≠ 1o
96 disjsn2 4711 . . . . . 6 (∅ ≠ 1o → ({∅} ∩ {1o}) = ∅)
9795, 96mp1i 13 . . . . 5 (𝜑 → ({∅} ∩ {1o}) = ∅)
9876, 77, 78, 79, 80, 81, 83, 89, 93, 97ptunhmeo 23800 . . . 4 (𝜑 → (𝑥 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})), 𝑦 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) ↦ (𝑥𝑦)) ∈ (((∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) ×t (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})))Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
99 fnpr2o 17567 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → {⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} Fn 2o)
1002, 3, 99syl2anc 582 . . . . . . . . 9 (𝜑 → {⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} Fn 2o)
1017prid1 4761 . . . . . . . . . 10 ∅ ∈ {∅, 1o}
102101, 90eleqtrri 2825 . . . . . . . . 9 ∅ ∈ 2o
103 fnressn 7164 . . . . . . . . 9 (({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} Fn 2o ∧ ∅ ∈ 2o) → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅}) = {⟨∅, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅)⟩})
104100, 102, 103sylancl 584 . . . . . . . 8 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅}) = {⟨∅, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅)⟩})
105 fvpr0o 17569 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅) = 𝐽)
1062, 105syl 17 . . . . . . . . . 10 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅) = 𝐽)
107106opeq2d 4878 . . . . . . . . 9 (𝜑 → ⟨∅, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅)⟩ = ⟨∅, 𝐽⟩)
108107sneqd 4635 . . . . . . . 8 (𝜑 → {⟨∅, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘∅)⟩} = {⟨∅, 𝐽⟩})
109104, 108eqtrd 2766 . . . . . . 7 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅}) = {⟨∅, 𝐽⟩})
110109fveq2d 6897 . . . . . 6 (𝜑 → (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
111110unieqd 4918 . . . . 5 (𝜑 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
112 1oex 8498 . . . . . . . . . . 11 1o ∈ V
113112prid2 4762 . . . . . . . . . 10 1o ∈ {∅, 1o}
114113, 90eleqtrri 2825 . . . . . . . . 9 1o ∈ 2o
115 fnressn 7164 . . . . . . . . 9 (({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} Fn 2o ∧ 1o ∈ 2o) → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}) = {⟨1o, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o)⟩})
116100, 114, 115sylancl 584 . . . . . . . 8 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}) = {⟨1o, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o)⟩})
117 fvpr1o 17570 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o) = 𝐾)
1183, 117syl 17 . . . . . . . . . 10 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o) = 𝐾)
119118opeq2d 4878 . . . . . . . . 9 (𝜑 → ⟨1o, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o)⟩ = ⟨1o, 𝐾⟩)
120119sneqd 4635 . . . . . . . 8 (𝜑 → {⟨1o, ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}‘1o)⟩} = {⟨1o, 𝐾⟩})
121116, 120eqtrd 2766 . . . . . . 7 (𝜑 → ({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}) = {⟨1o, 𝐾⟩})
122121fveq2d 6897 . . . . . 6 (𝜑 → (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) = (∏t‘{⟨1o, 𝐾⟩}))
123122unieqd 4918 . . . . 5 (𝜑 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) = (∏t‘{⟨1o, 𝐾⟩}))
124 eqidd 2727 . . . . 5 (𝜑 → (𝑥𝑦) = (𝑥𝑦))
125111, 123, 124mpoeq123dv 7492 . . . 4 (𝜑 → (𝑥 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})), 𝑦 (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})) ↦ (𝑥𝑦)) = (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)))
126110, 122oveq12d 7434 . . . . 5 (𝜑 → ((∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) ×t (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o}))) = ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))
127126oveq1d 7431 . . . 4 (𝜑 → (((∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {∅})) ×t (∏t‘({⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩} ↾ {1o})))Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})) = (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
12898, 125, 1273eltr3d 2840 . . 3 (𝜑 → (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
129 hmeoco 23764 . . 3 (((𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}))) → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
13049, 128, 129syl2anc 582 . 2 (𝜑 → ((𝑥 (∏t‘{⟨∅, 𝐽⟩}), 𝑦 (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥𝑦)) ∘ (𝑥𝑋, 𝑦𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
13175, 130eqeltrd 2826 1 (𝜑𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wne 2930  wral 3051  Vcvv 3462  cun 3944  cin 3945  c0 4322  {csn 4623  {cpr 4625  cop 4629   cuni 4905  cmpt 5228   × cxp 5672  cres 5676  ccom 5678  Oncon0 6368   Fn wfn 6541  wf 6542  cfv 6546  (class class class)co 7416  cmpo 7418  1st c1st 7993  2nd c2nd 7994  1oc1o 8481  2oc2o 8482  tcpt 17448  Topctop 22883  TopOnctopon 22900   Cn ccn 23216   ×t ctx 23552  Homeochmeo 23745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7995  df-2nd 7996  df-1o 8488  df-2o 8489  df-map 8849  df-ixp 8919  df-en 8967  df-dom 8968  df-fin 8970  df-fi 9447  df-topgen 17453  df-pt 17454  df-top 22884  df-topon 22901  df-bases 22937  df-cn 23219  df-cnp 23220  df-tx 23554  df-hmeo 23747
This theorem is referenced by:  xpstopnlem2  23803
  Copyright terms: Public domain W3C validator