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

Theorem ptunhmeo 22344
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 3495 . . . . . . . 8 𝑥 ∈ V
3 vex 3495 . . . . . . . 8 𝑦 ∈ V
42, 3op1std 7688 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
52, 3op2ndd 7689 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
64, 5uneq12d 4137 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
76mpompt 7255 . . . . 5 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2844 . . . 4 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧)))
9 xp1st 7710 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (1st𝑧) ∈ 𝑋)
109adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ 𝑋)
11 ixpeq2 8463 . . . . . . . . . . . . 13 (∀𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛))
12 fvres 6682 . . . . . . . . . . . . . 14 (𝑛𝐴 → ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1312unieqd 4840 . . . . . . . . . . . . 13 (𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1411, 13mprg 3149 . . . . . . . . . . . 12 X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛)
15 ptunhmeo.c . . . . . . . . . . . . . 14 (𝜑𝐶𝑉)
16 ssun1 4145 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . . . . 15 (𝜑𝐶 = (𝐴𝐵))
1816, 17sseqtrrid 4017 . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
1915, 18ssexd 5219 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6538 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . . . . 14 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 22130 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2419, 21, 23syl2anc 584 . . . . . . . . . . . 12 (𝜑X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2514, 24syl5eqr 2867 . . . . . . . . . . 11 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝐾)
26 ptunhmeo.x . . . . . . . . . . 11 𝑋 = 𝐾
2725, 26syl6eqr 2871 . . . . . . . . . 10 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝑋)
2827adantr 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
2910, 28eleqtrrd 2913 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛))
30 xp2nd 7711 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (2nd𝑧) ∈ 𝑌)
3130adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ 𝑌)
3217eqcomd 2824 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4434 . . . . . . . . . . . . . 14 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 233 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 8461 . . . . . . . . . . 11 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = X𝑛𝐵 (𝐹𝑛))
38 ixpeq2 8463 . . . . . . . . . . . . . 14 (∀𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛))
39 fvres 6682 . . . . . . . . . . . . . . 15 (𝑛𝐵 → ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4039unieqd 4840 . . . . . . . . . . . . . 14 (𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4138, 40mprg 3149 . . . . . . . . . . . . 13 X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛)
42 ssun2 4146 . . . . . . . . . . . . . . . 16 𝐵 ⊆ (𝐴𝐵)
4342, 17sseqtrrid 4017 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
4415, 43ssexd 5219 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ V)
4520, 43fssresd 6538 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . . . . 15 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 22130 . . . . . . . . . . . . . 14 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4844, 45, 47syl2anc 584 . . . . . . . . . . . . 13 (𝜑X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4941, 48syl5eqr 2867 . . . . . . . . . . . 12 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝐿)
50 ptunhmeo.y . . . . . . . . . . . 12 𝑌 = 𝐿
5149, 50syl6eqr 2871 . . . . . . . . . . 11 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝑌)
5237, 51eqtrd 2853 . . . . . . . . . 10 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5352adantr 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5431, 53eleqtrrd 2913 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛))
5518adantr 481 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 8486 . . . . . . . 8 (((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) ∧ (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) ∧ 𝐴𝐶) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
5729, 54, 55, 56syl3anc 1363 . . . . . . 7 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
58 ixpfn 8455 . . . . . . 7 (((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
5957, 58syl 17 . . . . . 6 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
60 dffn5 6717 . . . . . 6 (((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶 ↔ ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6159, 60sylib 219 . . . . 5 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6261mpteq2dva 5152 . . . 4 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
638, 62syl5eq 2865 . . 3 (𝜑𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
64 ptunhmeo.j . . . 4 𝐽 = (∏t𝐹)
65 pttop 22118 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → (∏t‘(𝐹𝐴)) ∈ Top)
6619, 21, 65syl2anc 584 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐴)) ∈ Top)
6722, 66eqeltrid 2914 . . . . . 6 (𝜑𝐾 ∈ Top)
6826toptopon 21453 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
6967, 68sylib 219 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑋))
70 pttop 22118 . . . . . . . 8 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
7144, 45, 70syl2anc 584 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐵)) ∈ Top)
7246, 71eqeltrid 2914 . . . . . 6 (𝜑𝐿 ∈ Top)
7350toptopon 21453 . . . . . 6 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
7472, 73sylib 219 . . . . 5 (𝜑𝐿 ∈ (TopOn‘𝑌))
75 txtopon 22127 . . . . 5 ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7669, 74, 75syl2anc 584 . . . 4 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7717eleq2d 2895 . . . . . . 7 (𝜑 → (𝑘𝐶𝑘 ∈ (𝐴𝐵)))
7877biimpa 477 . . . . . 6 ((𝜑𝑘𝐶) → 𝑘 ∈ (𝐴𝐵))
79 elun 4122 . . . . . 6 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
8078, 79sylib 219 . . . . 5 ((𝜑𝑘𝐶) → (𝑘𝐴𝑘𝐵))
81 ixpfn 8455 . . . . . . . . . . 11 ((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) → (1st𝑧) Fn 𝐴)
8229, 81syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8382adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8451adantr 481 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐵 (𝐹𝑛) = 𝑌)
8531, 84eleqtrrd 2913 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛))
86 ixpfn 8455 . . . . . . . . . . 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 6747 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐴)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9283, 88, 89, 90, 91syl112anc 1366 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9392mpteq2dva 5152 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)))
9476adantr 481 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
954mpompt 7255 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
9669adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐾 ∈ (TopOn‘𝑋))
9774adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐿 ∈ (TopOn‘𝑌))
9896, 97cnmpt1st 22204 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
9995, 98eqeltrid 2914 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
10019adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐴 ∈ V)
10121adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝐴):𝐴⟶Top)
102 simpr 485 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝑘𝐴)
10326, 22ptpjcn 22147 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top ∧ 𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
104100, 101, 102, 103syl3anc 1363 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
105 fvres 6682 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
106105adantl 482 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
107106oveq2d 7161 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐾 Cn ((𝐹𝐴)‘𝑘)) = (𝐾 Cn (𝐹𝑘)))
108104, 107eleqtrd 2912 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn (𝐹𝑘)))
109 fveq1 6662 . . . . . . . 8 (𝑓 = (1st𝑧) → (𝑓𝑘) = ((1st𝑧)‘𝑘))
11094, 99, 96, 108, 109cnmpt11 22199 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11193, 110eqeltrd 2910 . . . . . 6 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11282adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
11387adantlr 711 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
11433ad2antrr 722 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
115 simplr 765 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐵)
116 fvun2 6748 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐵)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
117112, 113, 114, 115, 116syl112anc 1366 . . . . . . . 8 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
118117mpteq2dva 5152 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)))
11976adantr 481 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
1205mpompt 7255 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) = (𝑥𝑋, 𝑦𝑌𝑦)
12169adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐾 ∈ (TopOn‘𝑋))
12274adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123121, 122cnmpt2nd 22205 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124120, 123eqeltrid 2914 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
12544adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐵 ∈ V)
12645adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → (𝐹𝐵):𝐵⟶Top)
127 simpr 485 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝑘𝐵)
12850, 46ptpjcn 22147 . . . . . . . . . 10 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top ∧ 𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
129125, 126, 127, 128syl3anc 1363 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
130 fvres 6682 . . . . . . . . . . 11 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
131130adantl 482 . . . . . . . . . 10 ((𝜑𝑘𝐵) → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
132131oveq2d 7161 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝐿 Cn ((𝐹𝐵)‘𝑘)) = (𝐿 Cn (𝐹𝑘)))
133129, 132eleqtrd 2912 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn (𝐹𝑘)))
134 fveq1 6662 . . . . . . . 8 (𝑓 = (2nd𝑧) → (𝑓𝑘) = ((2nd𝑧)‘𝑘))
135119, 124, 122, 133, 134cnmpt11 22199 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
136118, 135eqeltrd 2910 . . . . . 6 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
137111, 136jaodan 951 . . . . 5 ((𝜑 ∧ (𝑘𝐴𝑘𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13880, 137syldan 591 . . . 4 ((𝜑𝑘𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13964, 76, 15, 20, 138ptcn 22163 . . 3 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14063, 139eqeltrd 2910 . 2 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14126, 50, 64, 22, 46, 1, 15, 20, 17, 33ptuncnv 22343 . . 3 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
142 pttop 22118 . . . . . . 7 ((𝐶𝑉𝐹:𝐶⟶Top) → (∏t𝐹) ∈ Top)
14315, 20, 142syl2anc 584 . . . . . 6 (𝜑 → (∏t𝐹) ∈ Top)
14464, 143eqeltrid 2914 . . . . 5 (𝜑𝐽 ∈ Top)
145 eqid 2818 . . . . . 6 𝐽 = 𝐽
146145toptopon 21453 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
147144, 146sylib 219 . . . 4 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
148145, 64, 22ptrescn 22175 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐴𝐶) → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
14915, 20, 18, 148syl3anc 1363 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
150145, 64, 46ptrescn 22175 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐵𝐶) → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
15115, 20, 43, 150syl3anc 1363 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
152147, 149, 151cnmpt1t 22201 . . 3 (𝜑 → (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153141, 152eqeltrd 2910 . 2 (𝜑𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154 ishmeo 22295 . 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 841   = wceq 1528  wcel 2105  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  cop 4563   cuni 4830  cmpt 5137   × cxp 5546  ccnv 5547  cres 5550   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  1st c1st 7676  2nd c2nd 7677  Xcixp 8449  tcpt 16700  Topctop 21429  TopOnctopon 21446   Cn ccn 21760   ×t ctx 22096  Homeochmeo 22289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-ixp 8450  df-en 8498  df-dom 8499  df-fin 8501  df-fi 8863  df-topgen 16705  df-pt 16706  df-top 21430  df-topon 21447  df-bases 21482  df-cn 21763  df-cnp 21764  df-tx 22098  df-hmeo 22291
This theorem is referenced by:  xpstopnlem1  22345  ptcmpfi  22349
  Copyright terms: Public domain W3C validator