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

Theorem ptunhmeo 22423
 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 3444 . . . . . . . 8 𝑥 ∈ V
3 vex 3444 . . . . . . . 8 𝑦 ∈ V
42, 3op1std 7684 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
52, 3op2ndd 7685 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
64, 5uneq12d 4091 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
76mpompt 7246 . . . . 5 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2824 . . . 4 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧)))
9 xp1st 7706 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (1st𝑧) ∈ 𝑋)
109adantl 485 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ 𝑋)
11 ixpeq2 8461 . . . . . . . . . . . . 13 (∀𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛))
12 fvres 6665 . . . . . . . . . . . . . 14 (𝑛𝐴 → ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1312unieqd 4815 . . . . . . . . . . . . 13 (𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1411, 13mprg 3120 . . . . . . . . . . . 12 X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛)
15 ptunhmeo.c . . . . . . . . . . . . . 14 (𝜑𝐶𝑉)
16 ssun1 4099 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . . . . 15 (𝜑𝐶 = (𝐴𝐵))
1816, 17sseqtrrid 3968 . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
1915, 18ssexd 5193 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6520 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . . . . 14 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 22209 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2419, 21, 23syl2anc 587 . . . . . . . . . . . 12 (𝜑X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2514, 24syl5eqr 2847 . . . . . . . . . . 11 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝐾)
26 ptunhmeo.x . . . . . . . . . . 11 𝑋 = 𝐾
2725, 26eqtr4di 2851 . . . . . . . . . 10 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝑋)
2827adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
2910, 28eleqtrrd 2893 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛))
30 xp2nd 7707 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (2nd𝑧) ∈ 𝑌)
3130adantl 485 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ 𝑌)
3217eqcomd 2804 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4396 . . . . . . . . . . . . . 14 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 235 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 8459 . . . . . . . . . . 11 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = X𝑛𝐵 (𝐹𝑛))
38 ixpeq2 8461 . . . . . . . . . . . . . 14 (∀𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛))
39 fvres 6665 . . . . . . . . . . . . . . 15 (𝑛𝐵 → ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4039unieqd 4815 . . . . . . . . . . . . . 14 (𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4138, 40mprg 3120 . . . . . . . . . . . . 13 X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛)
42 ssun2 4100 . . . . . . . . . . . . . . . 16 𝐵 ⊆ (𝐴𝐵)
4342, 17sseqtrrid 3968 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
4415, 43ssexd 5193 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ V)
4520, 43fssresd 6520 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . . . . 15 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 22209 . . . . . . . . . . . . . 14 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4844, 45, 47syl2anc 587 . . . . . . . . . . . . 13 (𝜑X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4941, 48syl5eqr 2847 . . . . . . . . . . . 12 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝐿)
50 ptunhmeo.y . . . . . . . . . . . 12 𝑌 = 𝐿
5149, 50eqtr4di 2851 . . . . . . . . . . 11 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝑌)
5237, 51eqtrd 2833 . . . . . . . . . 10 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5352adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5431, 53eleqtrrd 2893 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛))
5518adantr 484 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 8484 . . . . . . . 8 (((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) ∧ (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) ∧ 𝐴𝐶) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
5729, 54, 55, 56syl3anc 1368 . . . . . . 7 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
58 ixpfn 8453 . . . . . . 7 (((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
5957, 58syl 17 . . . . . 6 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
60 dffn5 6700 . . . . . 6 (((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶 ↔ ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6159, 60sylib 221 . . . . 5 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6261mpteq2dva 5126 . . . 4 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
638, 62syl5eq 2845 . . 3 (𝜑𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
64 ptunhmeo.j . . . 4 𝐽 = (∏t𝐹)
65 pttop 22197 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → (∏t‘(𝐹𝐴)) ∈ Top)
6619, 21, 65syl2anc 587 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐴)) ∈ Top)
6722, 66eqeltrid 2894 . . . . . 6 (𝜑𝐾 ∈ Top)
6826toptopon 21532 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
6967, 68sylib 221 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑋))
70 pttop 22197 . . . . . . . 8 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
7144, 45, 70syl2anc 587 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐵)) ∈ Top)
7246, 71eqeltrid 2894 . . . . . 6 (𝜑𝐿 ∈ Top)
7350toptopon 21532 . . . . . 6 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
7472, 73sylib 221 . . . . 5 (𝜑𝐿 ∈ (TopOn‘𝑌))
75 txtopon 22206 . . . . 5 ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7669, 74, 75syl2anc 587 . . . 4 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7717eleq2d 2875 . . . . . . 7 (𝜑 → (𝑘𝐶𝑘 ∈ (𝐴𝐵)))
7877biimpa 480 . . . . . 6 ((𝜑𝑘𝐶) → 𝑘 ∈ (𝐴𝐵))
79 elun 4076 . . . . . 6 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
8078, 79sylib 221 . . . . 5 ((𝜑𝑘𝐶) → (𝑘𝐴𝑘𝐵))
81 ixpfn 8453 . . . . . . . . . . 11 ((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) → (1st𝑧) Fn 𝐴)
8229, 81syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8382adantlr 714 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8451adantr 484 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐵 (𝐹𝑛) = 𝑌)
8531, 84eleqtrrd 2893 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛))
86 ixpfn 8453 . . . . . . . . . . 11 ((2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛) → (2nd𝑧) Fn 𝐵)
8785, 86syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8887adantlr 714 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8933ad2antrr 725 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
90 simplr 768 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐴)
91 fvun1 6730 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐴)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9283, 88, 89, 90, 91syl112anc 1371 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9392mpteq2dva 5126 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)))
9476adantr 484 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
954mpompt 7246 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
9669adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐾 ∈ (TopOn‘𝑋))
9774adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐿 ∈ (TopOn‘𝑌))
9896, 97cnmpt1st 22283 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
9995, 98eqeltrid 2894 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
10019adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐴 ∈ V)
10121adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝐴):𝐴⟶Top)
102 simpr 488 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝑘𝐴)
10326, 22ptpjcn 22226 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top ∧ 𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
104100, 101, 102, 103syl3anc 1368 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
105 fvres 6665 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
106105adantl 485 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
107106oveq2d 7152 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐾 Cn ((𝐹𝐴)‘𝑘)) = (𝐾 Cn (𝐹𝑘)))
108104, 107eleqtrd 2892 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn (𝐹𝑘)))
109 fveq1 6645 . . . . . . . 8 (𝑓 = (1st𝑧) → (𝑓𝑘) = ((1st𝑧)‘𝑘))
11094, 99, 96, 108, 109cnmpt11 22278 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11193, 110eqeltrd 2890 . . . . . 6 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11282adantlr 714 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
11387adantlr 714 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
11433ad2antrr 725 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
115 simplr 768 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐵)
116 fvun2 6731 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐵)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
117112, 113, 114, 115, 116syl112anc 1371 . . . . . . . 8 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
118117mpteq2dva 5126 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)))
11976adantr 484 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
1205mpompt 7246 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) = (𝑥𝑋, 𝑦𝑌𝑦)
12169adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐾 ∈ (TopOn‘𝑋))
12274adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123121, 122cnmpt2nd 22284 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124120, 123eqeltrid 2894 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
12544adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐵 ∈ V)
12645adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝐵) → (𝐹𝐵):𝐵⟶Top)
127 simpr 488 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝑘𝐵)
12850, 46ptpjcn 22226 . . . . . . . . . 10 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top ∧ 𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
129125, 126, 127, 128syl3anc 1368 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
130 fvres 6665 . . . . . . . . . . 11 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
131130adantl 485 . . . . . . . . . 10 ((𝜑𝑘𝐵) → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
132131oveq2d 7152 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝐿 Cn ((𝐹𝐵)‘𝑘)) = (𝐿 Cn (𝐹𝑘)))
133129, 132eleqtrd 2892 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn (𝐹𝑘)))
134 fveq1 6645 . . . . . . . 8 (𝑓 = (2nd𝑧) → (𝑓𝑘) = ((2nd𝑧)‘𝑘))
135119, 124, 122, 133, 134cnmpt11 22278 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
136118, 135eqeltrd 2890 . . . . . 6 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
137111, 136jaodan 955 . . . . 5 ((𝜑 ∧ (𝑘𝐴𝑘𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13880, 137syldan 594 . . . 4 ((𝜑𝑘𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13964, 76, 15, 20, 138ptcn 22242 . . 3 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14063, 139eqeltrd 2890 . 2 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14126, 50, 64, 22, 46, 1, 15, 20, 17, 33ptuncnv 22422 . . 3 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
142 pttop 22197 . . . . . . 7 ((𝐶𝑉𝐹:𝐶⟶Top) → (∏t𝐹) ∈ Top)
14315, 20, 142syl2anc 587 . . . . . 6 (𝜑 → (∏t𝐹) ∈ Top)
14464, 143eqeltrid 2894 . . . . 5 (𝜑𝐽 ∈ Top)
145 eqid 2798 . . . . . 6 𝐽 = 𝐽
146145toptopon 21532 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
147144, 146sylib 221 . . . 4 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
148145, 64, 22ptrescn 22254 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐴𝐶) → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
14915, 20, 18, 148syl3anc 1368 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
150145, 64, 46ptrescn 22254 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐵𝐶) → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
15115, 20, 43, 150syl3anc 1368 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
152147, 149, 151cnmpt1t 22280 . . 3 (𝜑 → (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153141, 152eqeltrd 2890 . 2 (𝜑𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154 ishmeo 22374 . 2 (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ 𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))))
155140, 153, 154sylanbrc 586 1 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ⟨cop 4531  ∪ cuni 4801   ↦ cmpt 5111   × cxp 5518  ◡ccnv 5519   ↾ cres 5522   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136   ∈ cmpo 7138  1st c1st 7672  2nd c2nd 7673  Xcixp 8447  ∏tcpt 16707  Topctop 21508  TopOnctopon 21525   Cn ccn 21839   ×t ctx 22175  Homeochmeo 22368 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-map 8394  df-ixp 8448  df-en 8496  df-dom 8497  df-fin 8499  df-fi 8862  df-topgen 16712  df-pt 16713  df-top 21509  df-topon 21526  df-bases 21561  df-cn 21842  df-cnp 21843  df-tx 22177  df-hmeo 22370 This theorem is referenced by:  xpstopnlem1  22424  ptcmpfi  22428
 Copyright terms: Public domain W3C validator