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

Theorem ptunhmeo 21805
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 3335 . . . . . . . 8 𝑥 ∈ V
3 vex 3335 . . . . . . . 8 𝑦 ∈ V
42, 3op1std 7335 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
52, 3op2ndd 7336 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
64, 5uneq12d 3903 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
76mpt2mpt 6909 . . . . 5 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2777 . . . 4 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧)))
9 xp1st 7357 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (1st𝑧) ∈ 𝑋)
109adantl 473 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ 𝑋)
11 ixpeq2 8080 . . . . . . . . . . . . 13 (∀𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛))
12 fvres 6360 . . . . . . . . . . . . . 14 (𝑛𝐴 → ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1312unieqd 4590 . . . . . . . . . . . . 13 (𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1411, 13mprg 3056 . . . . . . . . . . . 12 X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛)
15 ptunhmeo.c . . . . . . . . . . . . . 14 (𝜑𝐶𝑉)
16 ssun1 3911 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . . . . 15 (𝜑𝐶 = (𝐴𝐵))
1816, 17syl5sseqr 3787 . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
1915, 18ssexd 4949 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6224 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . . . . 14 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 21591 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2419, 21, 23syl2anc 696 . . . . . . . . . . . 12 (𝜑X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2514, 24syl5eqr 2800 . . . . . . . . . . 11 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝐾)
26 ptunhmeo.x . . . . . . . . . . 11 𝑋 = 𝐾
2725, 26syl6eqr 2804 . . . . . . . . . 10 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝑋)
2827adantr 472 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
2910, 28eleqtrrd 2834 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛))
30 xp2nd 7358 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (2nd𝑧) ∈ 𝑌)
3130adantl 473 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ 𝑌)
3217eqcomd 2758 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4193 . . . . . . . . . . . . . 14 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 222 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 8078 . . . . . . . . . . 11 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = X𝑛𝐵 (𝐹𝑛))
38 ixpeq2 8080 . . . . . . . . . . . . . 14 (∀𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛))
39 fvres 6360 . . . . . . . . . . . . . . 15 (𝑛𝐵 → ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4039unieqd 4590 . . . . . . . . . . . . . 14 (𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4138, 40mprg 3056 . . . . . . . . . . . . 13 X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛)
42 ssun2 3912 . . . . . . . . . . . . . . . 16 𝐵 ⊆ (𝐴𝐵)
4342, 17syl5sseqr 3787 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
4415, 43ssexd 4949 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ V)
4520, 43fssresd 6224 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . . . . 15 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 21591 . . . . . . . . . . . . . 14 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4844, 45, 47syl2anc 696 . . . . . . . . . . . . 13 (𝜑X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4941, 48syl5eqr 2800 . . . . . . . . . . . 12 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝐿)
50 ptunhmeo.y . . . . . . . . . . . 12 𝑌 = 𝐿
5149, 50syl6eqr 2804 . . . . . . . . . . 11 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝑌)
5237, 51eqtrd 2786 . . . . . . . . . 10 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5352adantr 472 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5431, 53eleqtrrd 2834 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛))
5518adantr 472 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 8102 . . . . . . . 8 (((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) ∧ (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) ∧ 𝐴𝐶) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
5729, 54, 55, 56syl3anc 1473 . . . . . . 7 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
58 ixpfn 8072 . . . . . . 7 (((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
5957, 58syl 17 . . . . . 6 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
60 dffn5 6395 . . . . . 6 (((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶 ↔ ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6159, 60sylib 208 . . . . 5 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6261mpteq2dva 4888 . . . 4 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
638, 62syl5eq 2798 . . 3 (𝜑𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
64 ptunhmeo.j . . . 4 𝐽 = (∏t𝐹)
65 pttop 21579 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → (∏t‘(𝐹𝐴)) ∈ Top)
6619, 21, 65syl2anc 696 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐴)) ∈ Top)
6722, 66syl5eqel 2835 . . . . . 6 (𝜑𝐾 ∈ Top)
6826toptopon 20916 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
6967, 68sylib 208 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑋))
70 pttop 21579 . . . . . . . 8 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
7144, 45, 70syl2anc 696 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐵)) ∈ Top)
7246, 71syl5eqel 2835 . . . . . 6 (𝜑𝐿 ∈ Top)
7350toptopon 20916 . . . . . 6 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
7472, 73sylib 208 . . . . 5 (𝜑𝐿 ∈ (TopOn‘𝑌))
75 txtopon 21588 . . . . 5 ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7669, 74, 75syl2anc 696 . . . 4 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7717eleq2d 2817 . . . . . . 7 (𝜑 → (𝑘𝐶𝑘 ∈ (𝐴𝐵)))
7877biimpa 502 . . . . . 6 ((𝜑𝑘𝐶) → 𝑘 ∈ (𝐴𝐵))
79 elun 3888 . . . . . 6 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
8078, 79sylib 208 . . . . 5 ((𝜑𝑘𝐶) → (𝑘𝐴𝑘𝐵))
81 ixpfn 8072 . . . . . . . . . . 11 ((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) → (1st𝑧) Fn 𝐴)
8229, 81syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8382adantlr 753 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8451adantr 472 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐵 (𝐹𝑛) = 𝑌)
8531, 84eleqtrrd 2834 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛))
86 ixpfn 8072 . . . . . . . . . . 11 ((2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛) → (2nd𝑧) Fn 𝐵)
8785, 86syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8887adantlr 753 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8933ad2antrr 764 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
90 simplr 809 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐴)
91 fvun1 6423 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐴)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9283, 88, 89, 90, 91syl112anc 1477 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9392mpteq2dva 4888 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)))
9476adantr 472 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
954mpt2mpt 6909 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
9669adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐾 ∈ (TopOn‘𝑋))
9774adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐿 ∈ (TopOn‘𝑌))
9896, 97cnmpt1st 21665 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
9995, 98syl5eqel 2835 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
10019adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐴 ∈ V)
10121adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝐴):𝐴⟶Top)
102 simpr 479 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝑘𝐴)
10326, 22ptpjcn 21608 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top ∧ 𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
104100, 101, 102, 103syl3anc 1473 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
105 fvres 6360 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
106105adantl 473 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
107106oveq2d 6821 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐾 Cn ((𝐹𝐴)‘𝑘)) = (𝐾 Cn (𝐹𝑘)))
108104, 107eleqtrd 2833 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn (𝐹𝑘)))
109 fveq1 6343 . . . . . . . 8 (𝑓 = (1st𝑧) → (𝑓𝑘) = ((1st𝑧)‘𝑘))
11094, 99, 96, 108, 109cnmpt11 21660 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11193, 110eqeltrd 2831 . . . . . 6 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11282adantlr 753 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
11387adantlr 753 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
11433ad2antrr 764 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
115 simplr 809 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐵)
116 fvun2 6424 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐵)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
117112, 113, 114, 115, 116syl112anc 1477 . . . . . . . 8 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
118117mpteq2dva 4888 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)))
11976adantr 472 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
1205mpt2mpt 6909 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) = (𝑥𝑋, 𝑦𝑌𝑦)
12169adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐾 ∈ (TopOn‘𝑋))
12274adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123121, 122cnmpt2nd 21666 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124120, 123syl5eqel 2835 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
12544adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐵 ∈ V)
12645adantr 472 . . . . . . . . . 10 ((𝜑𝑘𝐵) → (𝐹𝐵):𝐵⟶Top)
127 simpr 479 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝑘𝐵)
12850, 46ptpjcn 21608 . . . . . . . . . 10 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top ∧ 𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
129125, 126, 127, 128syl3anc 1473 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
130 fvres 6360 . . . . . . . . . . 11 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
131130adantl 473 . . . . . . . . . 10 ((𝜑𝑘𝐵) → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
132131oveq2d 6821 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝐿 Cn ((𝐹𝐵)‘𝑘)) = (𝐿 Cn (𝐹𝑘)))
133129, 132eleqtrd 2833 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn (𝐹𝑘)))
134 fveq1 6343 . . . . . . . 8 (𝑓 = (2nd𝑧) → (𝑓𝑘) = ((2nd𝑧)‘𝑘))
135119, 124, 122, 133, 134cnmpt11 21660 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
136118, 135eqeltrd 2831 . . . . . 6 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
137111, 136jaodan 861 . . . . 5 ((𝜑 ∧ (𝑘𝐴𝑘𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13880, 137syldan 488 . . . 4 ((𝜑𝑘𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13964, 76, 15, 20, 138ptcn 21624 . . 3 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14063, 139eqeltrd 2831 . 2 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14126, 50, 64, 22, 46, 1, 15, 20, 17, 33ptuncnv 21804 . . 3 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
142 pttop 21579 . . . . . . 7 ((𝐶𝑉𝐹:𝐶⟶Top) → (∏t𝐹) ∈ Top)
14315, 20, 142syl2anc 696 . . . . . 6 (𝜑 → (∏t𝐹) ∈ Top)
14464, 143syl5eqel 2835 . . . . 5 (𝜑𝐽 ∈ Top)
145 eqid 2752 . . . . . 6 𝐽 = 𝐽
146145toptopon 20916 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
147144, 146sylib 208 . . . 4 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
148145, 64, 22ptrescn 21636 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐴𝐶) → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
14915, 20, 18, 148syl3anc 1473 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
150145, 64, 46ptrescn 21636 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐵𝐶) → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
15115, 20, 43, 150syl3anc 1473 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
152147, 149, 151cnmpt1t 21662 . . 3 (𝜑 → (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153141, 152eqeltrd 2831 . 2 (𝜑𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154 ishmeo 21756 . 2 (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ 𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))))
155140, 153, 154sylanbrc 701 1 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1624  wcel 2131  Vcvv 3332  cdif 3704  cun 3705  cin 3706  wss 3707  c0 4050  cop 4319   cuni 4580  cmpt 4873   × cxp 5256  ccnv 5257  cres 5260   Fn wfn 6036  wf 6037  cfv 6041  (class class class)co 6805  cmpt2 6807  1st c1st 7323  2nd c2nd 7324  Xcixp 8066  tcpt 16293  Topctop 20892  TopOnctopon 20909   Cn ccn 21222   ×t ctx 21557  Homeochmeo 21750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-er 7903  df-map 8017  df-ixp 8067  df-en 8114  df-dom 8115  df-fin 8117  df-fi 8474  df-topgen 16298  df-pt 16299  df-top 20893  df-topon 20910  df-bases 20944  df-cn 21225  df-cnp 21226  df-tx 21559  df-hmeo 21752
This theorem is referenced by:  xpstopnlem1  21806  ptcmpfi  21810
  Copyright terms: Public domain W3C validator