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

Theorem ptunhmeo 22100
Description: Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of (𝐴𝐵) · (𝐴𝐶) = 𝐴↑(𝐵 + 𝐶). (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
ptunhmeo.x 𝑋 = 𝐾
ptunhmeo.y 𝑌 = 𝐿
ptunhmeo.j 𝐽 = (∏t𝐹)
ptunhmeo.k 𝐾 = (∏t‘(𝐹𝐴))
ptunhmeo.l 𝐿 = (∏t‘(𝐹𝐵))
ptunhmeo.g 𝐺 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
ptunhmeo.c (𝜑𝐶𝑉)
ptunhmeo.f (𝜑𝐹:𝐶⟶Top)
ptunhmeo.u (𝜑𝐶 = (𝐴𝐵))
ptunhmeo.i (𝜑 → (𝐴𝐵) = ∅)
Assertion
Ref Expression
ptunhmeo (𝜑𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦   𝑥,𝐶,𝑦   𝑥,𝐹,𝑦   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝐺(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ptunhmeo
Dummy variables 𝑓 𝑘 𝑛 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptunhmeo.g . . . . 5 𝐺 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
2 vex 3439 . . . . . . . 8 𝑥 ∈ V
3 vex 3439 . . . . . . . 8 𝑦 ∈ V
42, 3op1std 7558 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
52, 3op2ndd 7559 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
64, 5uneq12d 4063 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
76mpompt 7125 . . . . 5 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2821 . . . 4 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧)))
9 xp1st 7580 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (1st𝑧) ∈ 𝑋)
109adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ 𝑋)
11 ixpeq2 8327 . . . . . . . . . . . . 13 (∀𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛))
12 fvres 6560 . . . . . . . . . . . . . 14 (𝑛𝐴 → ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1312unieqd 4757 . . . . . . . . . . . . 13 (𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1411, 13mprg 3118 . . . . . . . . . . . 12 X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛)
15 ptunhmeo.c . . . . . . . . . . . . . 14 (𝜑𝐶𝑉)
16 ssun1 4071 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . . . . 15 (𝜑𝐶 = (𝐴𝐵))
1816, 17sseqtrrid 3943 . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
1915, 18ssexd 5122 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6416 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . . . . 14 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 21886 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2419, 21, 23syl2anc 584 . . . . . . . . . . . 12 (𝜑X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2514, 24syl5eqr 2844 . . . . . . . . . . 11 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝐾)
26 ptunhmeo.x . . . . . . . . . . 11 𝑋 = 𝐾
2725, 26syl6eqr 2848 . . . . . . . . . 10 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝑋)
2827adantr 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
2910, 28eleqtrrd 2885 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛))
30 xp2nd 7581 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (2nd𝑧) ∈ 𝑌)
3130adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ 𝑌)
3217eqcomd 2800 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4354 . . . . . . . . . . . . . 14 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 233 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 8325 . . . . . . . . . . 11 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = X𝑛𝐵 (𝐹𝑛))
38 ixpeq2 8327 . . . . . . . . . . . . . 14 (∀𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛))
39 fvres 6560 . . . . . . . . . . . . . . 15 (𝑛𝐵 → ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4039unieqd 4757 . . . . . . . . . . . . . 14 (𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4138, 40mprg 3118 . . . . . . . . . . . . 13 X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛)
42 ssun2 4072 . . . . . . . . . . . . . . . 16 𝐵 ⊆ (𝐴𝐵)
4342, 17sseqtrrid 3943 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
4415, 43ssexd 5122 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ V)
4520, 43fssresd 6416 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . . . . 15 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 21886 . . . . . . . . . . . . . 14 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4844, 45, 47syl2anc 584 . . . . . . . . . . . . 13 (𝜑X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4941, 48syl5eqr 2844 . . . . . . . . . . . 12 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝐿)
50 ptunhmeo.y . . . . . . . . . . . 12 𝑌 = 𝐿
5149, 50syl6eqr 2848 . . . . . . . . . . 11 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝑌)
5237, 51eqtrd 2830 . . . . . . . . . 10 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5352adantr 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5431, 53eleqtrrd 2885 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛))
5518adantr 481 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 8349 . . . . . . . 8 (((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) ∧ (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) ∧ 𝐴𝐶) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
5729, 54, 55, 56syl3anc 1364 . . . . . . 7 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
58 ixpfn 8319 . . . . . . 7 (((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
5957, 58syl 17 . . . . . 6 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
60 dffn5 6595 . . . . . 6 (((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶 ↔ ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6159, 60sylib 219 . . . . 5 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6261mpteq2dva 5058 . . . 4 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
638, 62syl5eq 2842 . . 3 (𝜑𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
64 ptunhmeo.j . . . 4 𝐽 = (∏t𝐹)
65 pttop 21874 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → (∏t‘(𝐹𝐴)) ∈ Top)
6619, 21, 65syl2anc 584 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐴)) ∈ Top)
6722, 66syl5eqel 2886 . . . . . 6 (𝜑𝐾 ∈ Top)
6826toptopon 21209 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
6967, 68sylib 219 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑋))
70 pttop 21874 . . . . . . . 8 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
7144, 45, 70syl2anc 584 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐵)) ∈ Top)
7246, 71syl5eqel 2886 . . . . . 6 (𝜑𝐿 ∈ Top)
7350toptopon 21209 . . . . . 6 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
7472, 73sylib 219 . . . . 5 (𝜑𝐿 ∈ (TopOn‘𝑌))
75 txtopon 21883 . . . . 5 ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7669, 74, 75syl2anc 584 . . . 4 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7717eleq2d 2867 . . . . . . 7 (𝜑 → (𝑘𝐶𝑘 ∈ (𝐴𝐵)))
7877biimpa 477 . . . . . 6 ((𝜑𝑘𝐶) → 𝑘 ∈ (𝐴𝐵))
79 elun 4048 . . . . . 6 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
8078, 79sylib 219 . . . . 5 ((𝜑𝑘𝐶) → (𝑘𝐴𝑘𝐵))
81 ixpfn 8319 . . . . . . . . . . 11 ((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) → (1st𝑧) Fn 𝐴)
8229, 81syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8382adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8451adantr 481 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐵 (𝐹𝑛) = 𝑌)
8531, 84eleqtrrd 2885 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛))
86 ixpfn 8319 . . . . . . . . . . 11 ((2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛) → (2nd𝑧) Fn 𝐵)
8785, 86syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8887adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8933ad2antrr 722 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
90 simplr 765 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐴)
91 fvun1 6624 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐴)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9283, 88, 89, 90, 91syl112anc 1367 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9392mpteq2dva 5058 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)))
9476adantr 481 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
954mpompt 7125 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
9669adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐾 ∈ (TopOn‘𝑋))
9774adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐿 ∈ (TopOn‘𝑌))
9896, 97cnmpt1st 21960 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
9995, 98syl5eqel 2886 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
10019adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐴 ∈ V)
10121adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝐴):𝐴⟶Top)
102 simpr 485 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝑘𝐴)
10326, 22ptpjcn 21903 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top ∧ 𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
104100, 101, 102, 103syl3anc 1364 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
105 fvres 6560 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
106105adantl 482 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
107106oveq2d 7035 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐾 Cn ((𝐹𝐴)‘𝑘)) = (𝐾 Cn (𝐹𝑘)))
108104, 107eleqtrd 2884 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn (𝐹𝑘)))
109 fveq1 6540 . . . . . . . 8 (𝑓 = (1st𝑧) → (𝑓𝑘) = ((1st𝑧)‘𝑘))
11094, 99, 96, 108, 109cnmpt11 21955 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11193, 110eqeltrd 2882 . . . . . 6 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11282adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
11387adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
11433ad2antrr 722 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
115 simplr 765 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐵)
116 fvun2 6625 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐵)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
117112, 113, 114, 115, 116syl112anc 1367 . . . . . . . 8 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
118117mpteq2dva 5058 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)))
11976adantr 481 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
1205mpompt 7125 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) = (𝑥𝑋, 𝑦𝑌𝑦)
12169adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐾 ∈ (TopOn‘𝑋))
12274adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123121, 122cnmpt2nd 21961 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124120, 123syl5eqel 2886 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
12544adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐵 ∈ V)
12645adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → (𝐹𝐵):𝐵⟶Top)
127 simpr 485 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝑘𝐵)
12850, 46ptpjcn 21903 . . . . . . . . . 10 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top ∧ 𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
129125, 126, 127, 128syl3anc 1364 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
130 fvres 6560 . . . . . . . . . . 11 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
131130adantl 482 . . . . . . . . . 10 ((𝜑𝑘𝐵) → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
132131oveq2d 7035 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝐿 Cn ((𝐹𝐵)‘𝑘)) = (𝐿 Cn (𝐹𝑘)))
133129, 132eleqtrd 2884 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn (𝐹𝑘)))
134 fveq1 6540 . . . . . . . 8 (𝑓 = (2nd𝑧) → (𝑓𝑘) = ((2nd𝑧)‘𝑘))
135119, 124, 122, 133, 134cnmpt11 21955 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
136118, 135eqeltrd 2882 . . . . . 6 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
137111, 136jaodan 952 . . . . 5 ((𝜑 ∧ (𝑘𝐴𝑘𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13880, 137syldan 591 . . . 4 ((𝜑𝑘𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13964, 76, 15, 20, 138ptcn 21919 . . 3 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14063, 139eqeltrd 2882 . 2 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14126, 50, 64, 22, 46, 1, 15, 20, 17, 33ptuncnv 22099 . . 3 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
142 pttop 21874 . . . . . . 7 ((𝐶𝑉𝐹:𝐶⟶Top) → (∏t𝐹) ∈ Top)
14315, 20, 142syl2anc 584 . . . . . 6 (𝜑 → (∏t𝐹) ∈ Top)
14464, 143syl5eqel 2886 . . . . 5 (𝜑𝐽 ∈ Top)
145 eqid 2794 . . . . . 6 𝐽 = 𝐽
146145toptopon 21209 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
147144, 146sylib 219 . . . 4 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
148145, 64, 22ptrescn 21931 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐴𝐶) → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
14915, 20, 18, 148syl3anc 1364 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
150145, 64, 46ptrescn 21931 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐵𝐶) → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
15115, 20, 43, 150syl3anc 1364 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
152147, 149, 151cnmpt1t 21957 . . 3 (𝜑 → (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153141, 152eqeltrd 2882 . 2 (𝜑𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154 ishmeo 22051 . 2 (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ 𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))))
155140, 153, 154sylanbrc 583 1 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 842   = wceq 1522  wcel 2080  Vcvv 3436  cdif 3858  cun 3859  cin 3860  wss 3861  c0 4213  cop 4480   cuni 4747  cmpt 5043   × cxp 5444  ccnv 5445  cres 5448   Fn wfn 6223  wf 6224  cfv 6228  (class class class)co 7019  cmpo 7021  1st c1st 7546  2nd c2nd 7547  Xcixp 8313  tcpt 16541  Topctop 21185  TopOnctopon 21202   Cn ccn 21516   ×t ctx 21852  Homeochmeo 22045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-iin 4830  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-oadd 7960  df-er 8142  df-map 8261  df-ixp 8314  df-en 8361  df-dom 8362  df-fin 8364  df-fi 8724  df-topgen 16546  df-pt 16547  df-top 21186  df-topon 21203  df-bases 21238  df-cn 21519  df-cnp 21520  df-tx 21854  df-hmeo 22047
This theorem is referenced by:  xpstopnlem1  22101  ptcmpfi  22105
  Copyright terms: Public domain W3C validator