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

Theorem xkohmeo 23319
Description: The Exponential Law for topological spaces. The "currying" function 𝐹 is a homeomorphism on function spaces when 𝐽 and 𝐾 are exponentiable spaces (by xkococn 23164, it is sufficient to assume that 𝐽, 𝐾 are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
xkohmeo.x (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
xkohmeo.y (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
xkohmeo.f 𝐹 = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿) ↦ (π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦))))
xkohmeo.j (πœ‘ β†’ 𝐽 ∈ 𝑛-Locally Comp)
xkohmeo.k (πœ‘ β†’ 𝐾 ∈ 𝑛-Locally Comp)
xkohmeo.l (πœ‘ β†’ 𝐿 ∈ Top)
Assertion
Ref Expression
xkohmeo (πœ‘ β†’ 𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
Distinct variable groups:   π‘₯,𝑓,𝑦,𝐽   𝑓,𝐾,π‘₯,𝑦   πœ‘,𝑓,π‘₯,𝑦   𝑓,𝐿,π‘₯,𝑦   𝑓,𝑋,π‘₯,𝑦   𝑓,π‘Œ,π‘₯,𝑦   𝑓,𝐹,π‘₯,𝑦

Proof of Theorem xkohmeo
Dummy variables 𝑔 𝑑 𝑒 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkohmeo.f . . 3 𝐹 = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿) ↦ (π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦))))
2 xkohmeo.x . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
3 xkohmeo.y . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
4 txtopon 23095 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
52, 3, 4syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
6 topontop 22415 . . . . . 6 ((𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ Top)
75, 6syl 17 . . . . 5 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ Top)
8 xkohmeo.l . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9 eqid 2733 . . . . . 6 (𝐿 ↑ko (𝐽 Γ—t 𝐾)) = (𝐿 ↑ko (𝐽 Γ—t 𝐾))
109xkotopon 23104 . . . . 5 (((𝐽 Γ—t 𝐾) ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)))
117, 8, 10syl2anc 585 . . . 4 (πœ‘ β†’ (𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)))
12 vex 3479 . . . . . . . . 9 𝑓 ∈ V
13 vex 3479 . . . . . . . . 9 π‘₯ ∈ V
1412, 13op1std 7985 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (1st β€˜π‘§) = 𝑓)
1512, 13op2ndd 7986 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (2nd β€˜π‘§) = π‘₯)
16 eqidd 2734 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ 𝑦 = 𝑦)
1714, 15, 16oveq123d 7430 . . . . . . 7 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦) = (π‘₯𝑓𝑦))
1817mpteq2dv 5251 . . . . . 6 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))
1918mpompt 7522 . . . . 5 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))
20 txtopon 23095 . . . . . . 7 (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)) ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)))
2111, 2, 20syl2anc 585 . . . . . 6 (πœ‘ β†’ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)))
22 vex 3479 . . . . . . . . . . 11 𝑧 ∈ V
23 vex 3479 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7985 . . . . . . . . . 10 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (1st β€˜π‘€) = 𝑧)
2524fveq2d 6896 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (1st β€˜(1st β€˜π‘€)) = (1st β€˜π‘§))
2624fveq2d 6896 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (2nd β€˜(1st β€˜π‘€)) = (2nd β€˜π‘§))
2722, 23op2ndd 7986 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (2nd β€˜π‘€) = 𝑦)
2825, 26, 27oveq123d 7430 . . . . . . . 8 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)) = ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))
2928mpompt 7522 . . . . . . 7 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))
30 txtopon 23095 . . . . . . . . 9 ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) ∈ (TopOnβ€˜((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)))
3121, 3, 30syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) ∈ (TopOnβ€˜((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)))
32 toptopon2 22420 . . . . . . . . 9 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
338, 32sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
34 xkohmeo.j . . . . . . . . 9 (πœ‘ β†’ 𝐽 ∈ 𝑛-Locally Comp)
35 xkohmeo.k . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ 𝑛-Locally Comp)
36 txcmp 23147 . . . . . . . . . 10 ((π‘₯ ∈ Comp ∧ 𝑦 ∈ Comp) β†’ (π‘₯ Γ—t 𝑦) ∈ Comp)
3736txnlly 23141 . . . . . . . . 9 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐾 ∈ 𝑛-Locally Comp) β†’ (𝐽 Γ—t 𝐾) ∈ 𝑛-Locally Comp)
3834, 35, 37syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ 𝑛-Locally Comp)
3925mpompt 7522 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (1st β€˜(1st β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§))
405adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
4133adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
42 xp1st 8007 . . . . . . . . . . . . . . 15 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) β†’ (1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋))
4342adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋))
44 xp1st 8007 . . . . . . . . . . . . . 14 ((1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) β†’ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
4543, 44syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
46 cnf2 22753 . . . . . . . . . . . . 13 (((𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿)) β†’ (1st β€˜(1st β€˜π‘€)):(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐿)
4740, 41, 45, 46syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)):(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐿)
4847feqmptd 6961 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’)))
4948mpteq2dva 5249 . . . . . . . . . 10 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (1st β€˜(1st β€˜π‘€))) = (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))))
5039, 49eqtr3id 2787 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§)) = (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))))
5121, 3cnmpt1st 23172 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑧) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽)))
52 fveq2 6892 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ (1st β€˜π‘‘) = (1st β€˜π‘§))
5352cbvmptv 5262 . . . . . . . . . . 11 (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘‘)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§))
5414mpompt 7522 . . . . . . . . . . . 12 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§)) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ 𝑓)
5511, 2cnmpt1st 23172 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ 𝑓) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5654, 55eqeltrid 2838 . . . . . . . . . . 11 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5753, 56eqeltrid 2838 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘‘)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5821, 3, 51, 21, 57, 52cnmpt21 23175 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5950, 58eqeltrrd 2835 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
6026mpompt 7522 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜(1st β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (2nd β€˜π‘§))
61 fveq2 6892 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (2nd β€˜π‘‘) = (2nd β€˜π‘§))
6261cbvmptv 5262 . . . . . . . . . . . 12 (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘‘)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§))
6315mpompt 7522 . . . . . . . . . . . . 13 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§)) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ π‘₯)
6411, 2cnmpt2nd 23173 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6563, 64eqeltrid 2838 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6662, 65eqeltrid 2838 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘‘)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6721, 3, 51, 21, 66, 61cnmpt21 23175 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (2nd β€˜π‘§)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐽))
6860, 67eqeltrid 2838 . . . . . . . . 9 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜(1st β€˜π‘€))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐽))
6927mpompt 7522 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜π‘€)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑦)
7021, 3cnmpt2nd 23173 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐾))
7169, 70eqeltrid 2838 . . . . . . . . 9 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜π‘€)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐾))
7231, 68, 71cnmpt1t 23169 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐽 Γ—t 𝐾)))
73 fveq2 6892 . . . . . . . . 9 (𝑒 = ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩ β†’ ((1st β€˜(1st β€˜π‘€))β€˜π‘’) = ((1st β€˜(1st β€˜π‘€))β€˜βŸ¨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩))
74 df-ov 7412 . . . . . . . . 9 ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)) = ((1st β€˜(1st β€˜π‘€))β€˜βŸ¨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩)
7573, 74eqtr4di 2791 . . . . . . . 8 (𝑒 = ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩ β†’ ((1st β€˜(1st β€˜π‘€))β€˜π‘’) = ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)))
7631, 5, 33, 38, 59, 72, 75cnmptk1p 23189 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐿))
7729, 76eqeltrrid 2839 . . . . . 6 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐿))
7821, 3, 77cnmpt2k 23192 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko 𝐾)))
7919, 78eqeltrrid 2839 . . . 4 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦))) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko 𝐾)))
8011, 2, 79cnmpt2k 23192 . . 3 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿) ↦ (π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))) ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
811, 80eqeltrid 2838 . 2 (πœ‘ β†’ 𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
822, 3, 1, 34, 35, 8xkocnv 23318 . . . 4 (πœ‘ β†’ ◑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦))))
8313, 23op1std 7985 . . . . . . . 8 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘§) = π‘₯)
8483fveq2d 6896 . . . . . . 7 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (π‘”β€˜(1st β€˜π‘§)) = (π‘”β€˜π‘₯))
8513, 23op2ndd 7986 . . . . . . 7 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘§) = 𝑦)
8684, 85fveq12d 6899 . . . . . 6 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)) = ((π‘”β€˜π‘₯)β€˜π‘¦))
8786mpompt 7522 . . . . 5 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§))) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦))
8887mpteq2i 5254 . . . 4 (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦)))
8982, 88eqtr4di 2791 . . 3 (πœ‘ β†’ ◑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))))
90 nllytop 22977 . . . . . 6 (𝐽 ∈ 𝑛-Locally Comp β†’ 𝐽 ∈ Top)
9134, 90syl 17 . . . . 5 (πœ‘ β†’ 𝐽 ∈ Top)
92 nllytop 22977 . . . . . . 7 (𝐾 ∈ 𝑛-Locally Comp β†’ 𝐾 ∈ Top)
9335, 92syl 17 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ Top)
94 xkotop 23092 . . . . . 6 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko 𝐾) ∈ Top)
9593, 8, 94syl2anc 585 . . . . 5 (πœ‘ β†’ (𝐿 ↑ko 𝐾) ∈ Top)
96 eqid 2733 . . . . . 6 ((𝐿 ↑ko 𝐾) ↑ko 𝐽) = ((𝐿 ↑ko 𝐾) ↑ko 𝐽)
9796xkotopon 23104 . . . . 5 ((𝐽 ∈ Top ∧ (𝐿 ↑ko 𝐾) ∈ Top) β†’ ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))))
9891, 95, 97syl2anc 585 . . . 4 (πœ‘ β†’ ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))))
99 vex 3479 . . . . . . . . 9 𝑔 ∈ V
10099, 22op1std 7985 . . . . . . . 8 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (1st β€˜π‘€) = 𝑔)
10199, 22op2ndd 7986 . . . . . . . . 9 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (2nd β€˜π‘€) = 𝑧)
102101fveq2d 6896 . . . . . . . 8 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (1st β€˜(2nd β€˜π‘€)) = (1st β€˜π‘§))
103100, 102fveq12d 6899 . . . . . . 7 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) = (π‘”β€˜(1st β€˜π‘§)))
104101fveq2d 6896 . . . . . . 7 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (2nd β€˜(2nd β€˜π‘€)) = (2nd β€˜π‘§))
105103, 104fveq12d 6899 . . . . . 6 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€))) = ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))
106105mpompt 7522 . . . . 5 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))
107 txtopon 23095 . . . . . . 7 ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ))) β†’ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))))
10898, 5, 107syl2anc 585 . . . . . 6 (πœ‘ β†’ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))))
1093adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
11033adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
111 eqid 2733 . . . . . . . . . . . . . 14 (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
112111xkotopon 23104 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)))
11393, 8, 112syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)))
114 xp1st 8007 . . . . . . . . . . . 12 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) β†’ (1st β€˜π‘€) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
115 cnf2 22753 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)) ∧ (1st β€˜π‘€) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) β†’ (1st β€˜π‘€):π‘‹βŸΆ(𝐾 Cn 𝐿))
1162, 113, 114, 115syl2an3an 1423 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜π‘€):π‘‹βŸΆ(𝐾 Cn 𝐿))
117 xp2nd 8008 . . . . . . . . . . . . 13 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) β†’ (2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ))
118117adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ))
119 xp1st 8007 . . . . . . . . . . . 12 ((2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜(2nd β€˜π‘€)) ∈ 𝑋)
120118, 119syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜(2nd β€˜π‘€)) ∈ 𝑋)
121116, 120ffvelcdmd 7088 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) ∈ (𝐾 Cn 𝐿))
122 cnf2 22753 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) ∈ (𝐾 Cn 𝐿)) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))):π‘ŒβŸΆβˆͺ 𝐿)
123109, 110, 121, 122syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))):π‘ŒβŸΆβˆͺ 𝐿)
124123feqmptd 6961 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) = (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦)))
125124mpteq2dva 5249 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦))))
126100mpompt 7522 . . . . . . . . . 10 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜π‘€)) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔)
127116feqmptd 6961 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜π‘€) = (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯)))
128127mpteq2dva 5249 . . . . . . . . . 10 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜π‘€)) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))))
129126, 128eqtr3id 2787 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))))
13098, 5cnmpt1st 23172 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
131129, 130eqeltrrd 2835 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
132102mpompt 7522 . . . . . . . . 9 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜(2nd β€˜π‘€))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§))
13398, 5cnmpt2nd 23173 . . . . . . . . . 10 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑧) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐽 Γ—t 𝐾)))
13452cbvmptv 5262 . . . . . . . . . . 11 (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘‘)) = (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§))
13583mpompt 7522 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯)
1362, 3cnmpt1st 23172 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
137135, 136eqeltrid 2838 . . . . . . . . . . 11 (πœ‘ β†’ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
138134, 137eqeltrid 2838 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘‘)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
13998, 5, 133, 5, 138, 52cnmpt21 23175 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐽))
140132, 139eqeltrid 2838 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐽))
141 fveq2 6892 . . . . . . . 8 (π‘₯ = (1st β€˜(2nd β€˜π‘€)) β†’ ((1st β€˜π‘€)β€˜π‘₯) = ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))))
142108, 2, 113, 34, 131, 140, 141cnmptk1p 23189 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐿 ↑ko 𝐾)))
143125, 142eqeltrrd 2835 . . . . . 6 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐿 ↑ko 𝐾)))
144104mpompt 7522 . . . . . . 7 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (2nd β€˜(2nd β€˜π‘€))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§))
14561cbvmptv 5262 . . . . . . . . 9 (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘‘)) = (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§))
14685mpompt 7522 . . . . . . . . . 10 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦)
1472, 3cnmpt2nd 23173 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
148146, 147eqeltrid 2838 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
149145, 148eqeltrid 2838 . . . . . . . 8 (πœ‘ β†’ (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘‘)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
15098, 5, 133, 5, 149, 61cnmpt21 23175 . . . . . . 7 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐾))
151144, 150eqeltrid 2838 . . . . . 6 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (2nd β€˜(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐾))
152 fveq2 6892 . . . . . 6 (𝑦 = (2nd β€˜(2nd β€˜π‘€)) β†’ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦) = (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€))))
153108, 3, 33, 35, 143, 151, 152cnmptk1p 23189 . . . . 5 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐿))
154106, 153eqeltrrid 2839 . . . 4 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐿))
15598, 5, 154cnmpt2k 23192 . . 3 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))) ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
15689, 155eqeltrd 2834 . 2 (πœ‘ β†’ ◑𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
157 ishmeo 23263 . 2 (𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ↔ (𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ∧ ◑𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾)))))
15881, 156, 157sylanbrc 584 1 (πœ‘ β†’ 𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βŸ¨cop 4635  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1st c1st 7973  2nd c2nd 7974  Topctop 22395  TopOnctopon 22412   Cn ccn 22728  Compccmp 22890  π‘›-Locally cnlly 22969   Γ—t ctx 23064   ↑ko cxko 23065  Homeochmeo 23257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9406  df-rest 17368  df-topgen 17389  df-pt 17390  df-top 22396  df-topon 22413  df-bases 22449  df-ntr 22524  df-nei 22602  df-cn 22731  df-cnp 22732  df-cmp 22891  df-nlly 22971  df-tx 23066  df-xko 23067  df-hmeo 23259
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator