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

Theorem ptunhmeo 21659
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 3234 . . . . . . . 8 𝑥 ∈ V
3 vex 3234 . . . . . . . 8 𝑦 ∈ V
42, 3op1std 7220 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
52, 3op2ndd 7221 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
64, 5uneq12d 3801 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) ∪ (2nd𝑧)) = (𝑥𝑦))
76mpt2mpt 6794 . . . . 5 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑦))
81, 7eqtr4i 2676 . . . 4 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧)))
9 xp1st 7242 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (1st𝑧) ∈ 𝑋)
109adantl 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ 𝑋)
11 ixpeq2 7964 . . . . . . . . . . . . 13 (∀𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛))
12 fvres 6245 . . . . . . . . . . . . . 14 (𝑛𝐴 → ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1312unieqd 4478 . . . . . . . . . . . . 13 (𝑛𝐴 ((𝐹𝐴)‘𝑛) = (𝐹𝑛))
1411, 13mprg 2955 . . . . . . . . . . . 12 X𝑛𝐴 ((𝐹𝐴)‘𝑛) = X𝑛𝐴 (𝐹𝑛)
15 ptunhmeo.c . . . . . . . . . . . . . 14 (𝜑𝐶𝑉)
16 ssun1 3809 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴𝐵)
17 ptunhmeo.u . . . . . . . . . . . . . . 15 (𝜑𝐶 = (𝐴𝐵))
1816, 17syl5sseqr 3687 . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
1915, 18ssexd 4838 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
20 ptunhmeo.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐶⟶Top)
2120, 18fssresd 6109 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴):𝐴⟶Top)
22 ptunhmeo.k . . . . . . . . . . . . . 14 𝐾 = (∏t‘(𝐹𝐴))
2322ptuni 21445 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2419, 21, 23syl2anc 694 . . . . . . . . . . . 12 (𝜑X𝑛𝐴 ((𝐹𝐴)‘𝑛) = 𝐾)
2514, 24syl5eqr 2699 . . . . . . . . . . 11 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝐾)
26 ptunhmeo.x . . . . . . . . . . 11 𝑋 = 𝐾
2725, 26syl6eqr 2703 . . . . . . . . . 10 (𝜑X𝑛𝐴 (𝐹𝑛) = 𝑋)
2827adantr 480 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
2910, 28eleqtrrd 2733 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛))
30 xp2nd 7243 . . . . . . . . . 10 (𝑧 ∈ (𝑋 × 𝑌) → (2nd𝑧) ∈ 𝑌)
3130adantl 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ 𝑌)
3217eqcomd 2657 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = 𝐶)
33 ptunhmeo.i . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐵) = ∅)
34 uneqdifeq 4090 . . . . . . . . . . . . . 14 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3518, 33, 34syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
3632, 35mpbid 222 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐴) = 𝐵)
3736ixpeq1d 7962 . . . . . . . . . . 11 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = X𝑛𝐵 (𝐹𝑛))
38 ixpeq2 7964 . . . . . . . . . . . . . 14 (∀𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛))
39 fvres 6245 . . . . . . . . . . . . . . 15 (𝑛𝐵 → ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4039unieqd 4478 . . . . . . . . . . . . . 14 (𝑛𝐵 ((𝐹𝐵)‘𝑛) = (𝐹𝑛))
4138, 40mprg 2955 . . . . . . . . . . . . 13 X𝑛𝐵 ((𝐹𝐵)‘𝑛) = X𝑛𝐵 (𝐹𝑛)
42 ssun2 3810 . . . . . . . . . . . . . . . 16 𝐵 ⊆ (𝐴𝐵)
4342, 17syl5sseqr 3687 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
4415, 43ssexd 4838 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ V)
4520, 43fssresd 6109 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐵):𝐵⟶Top)
46 ptunhmeo.l . . . . . . . . . . . . . . 15 𝐿 = (∏t‘(𝐹𝐵))
4746ptuni 21445 . . . . . . . . . . . . . 14 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4844, 45, 47syl2anc 694 . . . . . . . . . . . . 13 (𝜑X𝑛𝐵 ((𝐹𝐵)‘𝑛) = 𝐿)
4941, 48syl5eqr 2699 . . . . . . . . . . . 12 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝐿)
50 ptunhmeo.y . . . . . . . . . . . 12 𝑌 = 𝐿
5149, 50syl6eqr 2703 . . . . . . . . . . 11 (𝜑X𝑛𝐵 (𝐹𝑛) = 𝑌)
5237, 51eqtrd 2685 . . . . . . . . . 10 (𝜑X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5352adantr 480 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) = 𝑌)
5431, 53eleqtrrd 2733 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛))
5518adantr 480 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → 𝐴𝐶)
56 undifixp 7986 . . . . . . . 8 (((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) ∧ (2nd𝑧) ∈ X𝑛 ∈ (𝐶𝐴) (𝐹𝑛) ∧ 𝐴𝐶) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
5729, 54, 55, 56syl3anc 1366 . . . . . . 7 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛))
58 ixpfn 7956 . . . . . . 7 (((1st𝑧) ∪ (2nd𝑧)) ∈ X𝑛𝐶 (𝐹𝑛) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
5957, 58syl 17 . . . . . 6 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶)
60 dffn5 6280 . . . . . 6 (((1st𝑧) ∪ (2nd𝑧)) Fn 𝐶 ↔ ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6159, 60sylib 208 . . . . 5 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → ((1st𝑧) ∪ (2nd𝑧)) = (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)))
6261mpteq2dva 4777 . . . 4 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧) ∪ (2nd𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
638, 62syl5eq 2697 . . 3 (𝜑𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))))
64 ptunhmeo.j . . . 4 𝐽 = (∏t𝐹)
65 pttop 21433 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top) → (∏t‘(𝐹𝐴)) ∈ Top)
6619, 21, 65syl2anc 694 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐴)) ∈ Top)
6722, 66syl5eqel 2734 . . . . . 6 (𝜑𝐾 ∈ Top)
6826toptopon 20770 . . . . . 6 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
6967, 68sylib 208 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑋))
70 pttop 21433 . . . . . . . 8 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
7144, 45, 70syl2anc 694 . . . . . . 7 (𝜑 → (∏t‘(𝐹𝐵)) ∈ Top)
7246, 71syl5eqel 2734 . . . . . 6 (𝜑𝐿 ∈ Top)
7350toptopon 20770 . . . . . 6 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
7472, 73sylib 208 . . . . 5 (𝜑𝐿 ∈ (TopOn‘𝑌))
75 txtopon 21442 . . . . 5 ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7669, 74, 75syl2anc 694 . . . 4 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
7717eleq2d 2716 . . . . . . 7 (𝜑 → (𝑘𝐶𝑘 ∈ (𝐴𝐵)))
7877biimpa 500 . . . . . 6 ((𝜑𝑘𝐶) → 𝑘 ∈ (𝐴𝐵))
79 elun 3786 . . . . . 6 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
8078, 79sylib 208 . . . . 5 ((𝜑𝑘𝐶) → (𝑘𝐴𝑘𝐵))
81 ixpfn 7956 . . . . . . . . . . 11 ((1st𝑧) ∈ X𝑛𝐴 (𝐹𝑛) → (1st𝑧) Fn 𝐴)
8229, 81syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8382adantlr 751 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
8451adantr 480 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → X𝑛𝐵 (𝐹𝑛) = 𝑌)
8531, 84eleqtrrd 2733 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛))
86 ixpfn 7956 . . . . . . . . . . 11 ((2nd𝑧) ∈ X𝑛𝐵 (𝐹𝑛) → (2nd𝑧) Fn 𝐵)
8785, 86syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8887adantlr 751 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
8933ad2antrr 762 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
90 simplr 807 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐴)
91 fvun1 6308 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐴)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9283, 88, 89, 90, 91syl112anc 1370 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((1st𝑧)‘𝑘))
9392mpteq2dva 4777 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)))
9476adantr 480 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
954mpt2mpt 6794 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
9669adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐾 ∈ (TopOn‘𝑋))
9774adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐿 ∈ (TopOn‘𝑌))
9896, 97cnmpt1st 21519 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
9995, 98syl5eqel 2734 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
10019adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐴 ∈ V)
10121adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝐴):𝐴⟶Top)
102 simpr 476 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝑘𝐴)
10326, 22ptpjcn 21462 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝐹𝐴):𝐴⟶Top ∧ 𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
104100, 101, 102, 103syl3anc 1366 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn ((𝐹𝐴)‘𝑘)))
105 fvres 6245 . . . . . . . . . . 11 (𝑘𝐴 → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
106105adantl 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝐴)‘𝑘) = (𝐹𝑘))
107106oveq2d 6706 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐾 Cn ((𝐹𝐴)‘𝑘)) = (𝐾 Cn (𝐹𝑘)))
108104, 107eleqtrd 2732 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑓𝑋 ↦ (𝑓𝑘)) ∈ (𝐾 Cn (𝐹𝑘)))
109 fveq1 6228 . . . . . . . 8 (𝑓 = (1st𝑧) → (𝑓𝑘) = ((1st𝑧)‘𝑘))
11094, 99, 96, 108, 109cnmpt11 21514 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11193, 110eqeltrd 2730 . . . . . 6 ((𝜑𝑘𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
11282adantlr 751 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st𝑧) Fn 𝐴)
11387adantlr 751 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd𝑧) Fn 𝐵)
11433ad2antrr 762 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴𝐵) = ∅)
115 simplr 807 . . . . . . . . 9 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘𝐵)
116 fvun2 6309 . . . . . . . . 9 (((1st𝑧) Fn 𝐴 ∧ (2nd𝑧) Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑘𝐵)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
117112, 113, 114, 115, 116syl112anc 1370 . . . . . . . 8 (((𝜑𝑘𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st𝑧) ∪ (2nd𝑧))‘𝑘) = ((2nd𝑧)‘𝑘))
118117mpteq2dva 4777 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)))
11976adantr 480 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
1205mpt2mpt 6794 . . . . . . . . 9 (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) = (𝑥𝑋, 𝑦𝑌𝑦)
12169adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐾 ∈ (TopOn‘𝑋))
12274adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123121, 122cnmpt2nd 21520 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124120, 123syl5eqel 2734 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
12544adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝐵 ∈ V)
12645adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐵) → (𝐹𝐵):𝐵⟶Top)
127 simpr 476 . . . . . . . . . 10 ((𝜑𝑘𝐵) → 𝑘𝐵)
12850, 46ptpjcn 21462 . . . . . . . . . 10 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top ∧ 𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
129125, 126, 127, 128syl3anc 1366 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn ((𝐹𝐵)‘𝑘)))
130 fvres 6245 . . . . . . . . . . 11 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
131130adantl 481 . . . . . . . . . 10 ((𝜑𝑘𝐵) → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
132131oveq2d 6706 . . . . . . . . 9 ((𝜑𝑘𝐵) → (𝐿 Cn ((𝐹𝐵)‘𝑘)) = (𝐿 Cn (𝐹𝑘)))
133129, 132eleqtrd 2732 . . . . . . . 8 ((𝜑𝑘𝐵) → (𝑓𝑌 ↦ (𝑓𝑘)) ∈ (𝐿 Cn (𝐹𝑘)))
134 fveq1 6228 . . . . . . . 8 (𝑓 = (2nd𝑧) → (𝑓𝑘) = ((2nd𝑧)‘𝑘))
135119, 124, 122, 133, 134cnmpt11 21514 . . . . . . 7 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
136118, 135eqeltrd 2730 . . . . . 6 ((𝜑𝑘𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
137111, 136jaodan 843 . . . . 5 ((𝜑 ∧ (𝑘𝐴𝑘𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13880, 137syldan 486 . . . 4 ((𝜑𝑘𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹𝑘)))
13964, 76, 15, 20, 138ptcn 21478 . . 3 (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘𝐶 ↦ (((1st𝑧) ∪ (2nd𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14063, 139eqeltrd 2730 . 2 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
14126, 50, 64, 22, 46, 1, 15, 20, 17, 33ptuncnv 21658 . . 3 (𝜑𝐺 = (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩))
142 pttop 21433 . . . . . . 7 ((𝐶𝑉𝐹:𝐶⟶Top) → (∏t𝐹) ∈ Top)
14315, 20, 142syl2anc 694 . . . . . 6 (𝜑 → (∏t𝐹) ∈ Top)
14464, 143syl5eqel 2734 . . . . 5 (𝜑𝐽 ∈ Top)
145 eqid 2651 . . . . . 6 𝐽 = 𝐽
146145toptopon 20770 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
147144, 146sylib 208 . . . 4 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
148145, 64, 22ptrescn 21490 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐴𝐶) → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
14915, 20, 18, 148syl3anc 1366 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐴)) ∈ (𝐽 Cn 𝐾))
150145, 64, 46ptrescn 21490 . . . . 5 ((𝐶𝑉𝐹:𝐶⟶Top ∧ 𝐵𝐶) → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
15115, 20, 43, 150syl3anc 1366 . . . 4 (𝜑 → (𝑧 𝐽 ↦ (𝑧𝐵)) ∈ (𝐽 Cn 𝐿))
152147, 149, 151cnmpt1t 21516 . . 3 (𝜑 → (𝑧 𝐽 ↦ ⟨(𝑧𝐴), (𝑧𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153141, 152eqeltrd 2730 . 2 (𝜑𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154 ishmeo 21610 . 2 (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ 𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))))
155140, 153, 154sylanbrc 699 1 (𝜑𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  cop 4216   cuni 4468  cmpt 4762   × cxp 5141  ccnv 5142  cres 5145   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  1st c1st 7208  2nd c2nd 7209  Xcixp 7950  tcpt 16146  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411  Homeochmeo 21604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-fin 8001  df-fi 8358  df-topgen 16151  df-pt 16152  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-cnp 21080  df-tx 21413  df-hmeo 21606
This theorem is referenced by:  xpstopnlem1  21660  ptcmpfi  21664
  Copyright terms: Public domain W3C validator