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

Theorem xkohmeo 23326
Description: The Exponential Law for topological spaces. The "currying" function 𝐹 is a homeomorphism on function spaces when 𝐽 and 𝐾 are exponentiable spaces (by xkococn 23171, 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 23102 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
52, 3, 4syl2anc 584 . . . . . 6 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
6 topontop 22422 . . . . . 6 ((𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ Top)
75, 6syl 17 . . . . 5 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ Top)
8 xkohmeo.l . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9 eqid 2732 . . . . . 6 (𝐿 ↑ko (𝐽 Γ—t 𝐾)) = (𝐿 ↑ko (𝐽 Γ—t 𝐾))
109xkotopon 23111 . . . . 5 (((𝐽 Γ—t 𝐾) ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)))
117, 8, 10syl2anc 584 . . . 4 (πœ‘ β†’ (𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)))
12 vex 3478 . . . . . . . . 9 𝑓 ∈ V
13 vex 3478 . . . . . . . . 9 π‘₯ ∈ V
1412, 13op1std 7987 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (1st β€˜π‘§) = 𝑓)
1512, 13op2ndd 7988 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (2nd β€˜π‘§) = π‘₯)
16 eqidd 2733 . . . . . . . 8 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ 𝑦 = 𝑦)
1714, 15, 16oveq123d 7432 . . . . . . 7 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦) = (π‘₯𝑓𝑦))
1817mpteq2dv 5250 . . . . . 6 (𝑧 = βŸ¨π‘“, π‘₯⟩ β†’ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))
1918mpompt 7524 . . . . 5 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))
20 txtopon 23102 . . . . . . 7 (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Γ—t 𝐾) Cn 𝐿)) ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)))
2111, 2, 20syl2anc 584 . . . . . 6 (πœ‘ β†’ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)))
22 vex 3478 . . . . . . . . . . 11 𝑧 ∈ V
23 vex 3478 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7987 . . . . . . . . . 10 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (1st β€˜π‘€) = 𝑧)
2524fveq2d 6895 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (1st β€˜(1st β€˜π‘€)) = (1st β€˜π‘§))
2624fveq2d 6895 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (2nd β€˜(1st β€˜π‘€)) = (2nd β€˜π‘§))
2722, 23op2ndd 7988 . . . . . . . . 9 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ (2nd β€˜π‘€) = 𝑦)
2825, 26, 27oveq123d 7432 . . . . . . . 8 (𝑀 = βŸ¨π‘§, π‘¦βŸ© β†’ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)) = ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))
2928mpompt 7524 . . . . . . 7 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))
30 txtopon 23102 . . . . . . . . 9 ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) ∈ (TopOnβ€˜(((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋)) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) ∈ (TopOnβ€˜((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)))
3121, 3, 30syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) ∈ (TopOnβ€˜((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)))
32 toptopon2 22427 . . . . . . . . 9 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
338, 32sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
34 xkohmeo.j . . . . . . . . 9 (πœ‘ β†’ 𝐽 ∈ 𝑛-Locally Comp)
35 xkohmeo.k . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ 𝑛-Locally Comp)
36 txcmp 23154 . . . . . . . . . 10 ((π‘₯ ∈ Comp ∧ 𝑦 ∈ Comp) β†’ (π‘₯ Γ—t 𝑦) ∈ Comp)
3736txnlly 23148 . . . . . . . . 9 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐾 ∈ 𝑛-Locally Comp) β†’ (𝐽 Γ—t 𝐾) ∈ 𝑛-Locally Comp)
3834, 35, 37syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ 𝑛-Locally Comp)
3925mpompt 7524 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (1st β€˜(1st β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§))
405adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
4133adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
42 xp1st 8009 . . . . . . . . . . . . . . 15 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) β†’ (1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋))
4342adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋))
44 xp1st 8009 . . . . . . . . . . . . . 14 ((1st β€˜π‘€) ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) β†’ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
4543, 44syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
46 cnf2 22760 . . . . . . . . . . . . 13 (((𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ (1st β€˜(1st β€˜π‘€)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿)) β†’ (1st β€˜(1st β€˜π‘€)):(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐿)
4740, 41, 45, 46syl3anc 1371 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)):(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐿)
4847feqmptd 6960 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ)) β†’ (1st β€˜(1st β€˜π‘€)) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’)))
4948mpteq2dva 5248 . . . . . . . . . 10 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (1st β€˜(1st β€˜π‘€))) = (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))))
5039, 49eqtr3id 2786 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§)) = (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))))
5121, 3cnmpt1st 23179 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑧) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽)))
52 fveq2 6891 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ (1st β€˜π‘‘) = (1st β€˜π‘§))
5352cbvmptv 5261 . . . . . . . . . . 11 (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘‘)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§))
5414mpompt 7524 . . . . . . . . . . . 12 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§)) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ 𝑓)
5511, 2cnmpt1st 23179 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ 𝑓) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5654, 55eqeltrid 2837 . . . . . . . . . . 11 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘§)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5753, 56eqeltrid 2837 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (1st β€˜π‘‘)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5821, 3, 51, 21, 57, 52cnmpt21 23182 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (1st β€˜π‘§)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
5950, 58eqeltrrd 2834 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ((1st β€˜(1st β€˜π‘€))β€˜π‘’))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
6026mpompt 7524 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜(1st β€˜π‘€))) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (2nd β€˜π‘§))
61 fveq2 6891 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (2nd β€˜π‘‘) = (2nd β€˜π‘§))
6261cbvmptv 5261 . . . . . . . . . . . 12 (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘‘)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§))
6315mpompt 7524 . . . . . . . . . . . . 13 (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§)) = (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ π‘₯)
6411, 2cnmpt2nd 23180 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6563, 64eqeltrid 2837 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘§)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6662, 65eqeltrid 2837 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (2nd β€˜π‘‘)) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn 𝐽))
6721, 3, 51, 21, 66, 61cnmpt21 23182 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ (2nd β€˜π‘§)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐽))
6860, 67eqeltrid 2837 . . . . . . . . 9 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜(1st β€˜π‘€))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐽))
6927mpompt 7524 . . . . . . . . . 10 (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜π‘€)) = (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑦)
7021, 3cnmpt2nd 23180 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐾))
7169, 70eqeltrid 2837 . . . . . . . . 9 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ (2nd β€˜π‘€)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐾))
7231, 68, 71cnmpt1t 23176 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn (𝐽 Γ—t 𝐾)))
73 fveq2 6891 . . . . . . . . 9 (𝑒 = ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩ β†’ ((1st β€˜(1st β€˜π‘€))β€˜π‘’) = ((1st β€˜(1st β€˜π‘€))β€˜βŸ¨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩))
74 df-ov 7414 . . . . . . . . 9 ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)) = ((1st β€˜(1st β€˜π‘€))β€˜βŸ¨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩)
7573, 74eqtr4di 2790 . . . . . . . 8 (𝑒 = ⟨(2nd β€˜(1st β€˜π‘€)), (2nd β€˜π‘€)⟩ β†’ ((1st β€˜(1st β€˜π‘€))β€˜π‘’) = ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€)))
7631, 5, 33, 38, 59, 72, 75cnmptk1p 23196 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) Γ— π‘Œ) ↦ ((2nd β€˜(1st β€˜π‘€))(1st β€˜(1st β€˜π‘€))(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐿))
7729, 76eqeltrrid 2838 . . . . . 6 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋), 𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦)) ∈ ((((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Γ—t 𝐾) Cn 𝐿))
7821, 3, 77cnmpt2k 23199 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (((𝐽 Γ—t 𝐾) Cn 𝐿) Γ— 𝑋) ↦ (𝑦 ∈ π‘Œ ↦ ((2nd β€˜π‘§)(1st β€˜π‘§)𝑦))) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko 𝐾)))
7919, 78eqeltrrid 2838 . . . 4 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿), π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦))) ∈ (((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Γ—t 𝐽) Cn (𝐿 ↑ko 𝐾)))
8011, 2, 79cnmpt2k 23199 . . 3 (πœ‘ β†’ (𝑓 ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿) ↦ (π‘₯ ∈ 𝑋 ↦ (𝑦 ∈ π‘Œ ↦ (π‘₯𝑓𝑦)))) ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
811, 80eqeltrid 2837 . 2 (πœ‘ β†’ 𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
822, 3, 1, 34, 35, 8xkocnv 23325 . . . 4 (πœ‘ β†’ ◑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦))))
8313, 23op1std 7987 . . . . . . . 8 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘§) = π‘₯)
8483fveq2d 6895 . . . . . . 7 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (π‘”β€˜(1st β€˜π‘§)) = (π‘”β€˜π‘₯))
8513, 23op2ndd 7988 . . . . . . 7 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘§) = 𝑦)
8684, 85fveq12d 6898 . . . . . 6 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)) = ((π‘”β€˜π‘₯)β€˜π‘¦))
8786mpompt 7524 . . . . 5 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§))) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦))
8887mpteq2i 5253 . . . 4 (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ((π‘”β€˜π‘₯)β€˜π‘¦)))
8982, 88eqtr4di 2790 . . 3 (πœ‘ β†’ ◑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))))
90 nllytop 22984 . . . . . 6 (𝐽 ∈ 𝑛-Locally Comp β†’ 𝐽 ∈ Top)
9134, 90syl 17 . . . . 5 (πœ‘ β†’ 𝐽 ∈ Top)
92 nllytop 22984 . . . . . . 7 (𝐾 ∈ 𝑛-Locally Comp β†’ 𝐾 ∈ Top)
9335, 92syl 17 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ Top)
94 xkotop 23099 . . . . . 6 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko 𝐾) ∈ Top)
9593, 8, 94syl2anc 584 . . . . 5 (πœ‘ β†’ (𝐿 ↑ko 𝐾) ∈ Top)
96 eqid 2732 . . . . . 6 ((𝐿 ↑ko 𝐾) ↑ko 𝐽) = ((𝐿 ↑ko 𝐾) ↑ko 𝐽)
9796xkotopon 23111 . . . . 5 ((𝐽 ∈ Top ∧ (𝐿 ↑ko 𝐾) ∈ Top) β†’ ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))))
9891, 95, 97syl2anc 584 . . . 4 (πœ‘ β†’ ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))))
99 vex 3478 . . . . . . . . 9 𝑔 ∈ V
10099, 22op1std 7987 . . . . . . . 8 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (1st β€˜π‘€) = 𝑔)
10199, 22op2ndd 7988 . . . . . . . . 9 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (2nd β€˜π‘€) = 𝑧)
102101fveq2d 6895 . . . . . . . 8 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (1st β€˜(2nd β€˜π‘€)) = (1st β€˜π‘§))
103100, 102fveq12d 6898 . . . . . . 7 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) = (π‘”β€˜(1st β€˜π‘§)))
104101fveq2d 6895 . . . . . . 7 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (2nd β€˜(2nd β€˜π‘€)) = (2nd β€˜π‘§))
105103, 104fveq12d 6898 . . . . . 6 (𝑀 = βŸ¨π‘”, π‘§βŸ© β†’ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€))) = ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))
106105mpompt 7524 . . . . 5 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))
107 txtopon 23102 . . . . . . 7 ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOnβ€˜(𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ))) β†’ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))))
10898, 5, 107syl2anc 584 . . . . . 6 (πœ‘ β†’ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) ∈ (TopOnβ€˜((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))))
1093adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
11033adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
111 eqid 2732 . . . . . . . . . . . . . 14 (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
112111xkotopon 23111 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)))
11393, 8, 112syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)))
114 xp1st 8009 . . . . . . . . . . . 12 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) β†’ (1st β€˜π‘€) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
115 cnf2 22760 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOnβ€˜(𝐾 Cn 𝐿)) ∧ (1st β€˜π‘€) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) β†’ (1st β€˜π‘€):π‘‹βŸΆ(𝐾 Cn 𝐿))
1162, 113, 114, 115syl2an3an 1422 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜π‘€):π‘‹βŸΆ(𝐾 Cn 𝐿))
117 xp2nd 8010 . . . . . . . . . . . . 13 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) β†’ (2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ))
118117adantl 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ))
119 xp1st 8009 . . . . . . . . . . . 12 ((2nd β€˜π‘€) ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜(2nd β€˜π‘€)) ∈ 𝑋)
120118, 119syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜(2nd β€˜π‘€)) ∈ 𝑋)
121116, 120ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) ∈ (𝐾 Cn 𝐿))
122 cnf2 22760 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) ∈ (𝐾 Cn 𝐿)) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))):π‘ŒβŸΆβˆͺ 𝐿)
123109, 110, 121, 122syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))):π‘ŒβŸΆβˆͺ 𝐿)
124123feqmptd 6960 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))) = (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦)))
125124mpteq2dva 5248 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦))))
126100mpompt 7524 . . . . . . . . . 10 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜π‘€)) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔)
127116feqmptd 6960 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ))) β†’ (1st β€˜π‘€) = (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯)))
128127mpteq2dva 5248 . . . . . . . . . 10 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜π‘€)) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))))
129126, 128eqtr3id 2786 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔) = (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))))
13098, 5cnmpt1st 23179 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑔) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
131129, 130eqeltrrd 2834 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (π‘₯ ∈ 𝑋 ↦ ((1st β€˜π‘€)β€˜π‘₯))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
132102mpompt 7524 . . . . . . . . 9 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜(2nd β€˜π‘€))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§))
13398, 5cnmpt2nd 23180 . . . . . . . . . 10 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ 𝑧) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐽 Γ—t 𝐾)))
13452cbvmptv 5261 . . . . . . . . . . 11 (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘‘)) = (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§))
13583mpompt 7524 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯)
1362, 3cnmpt1st 23179 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
137135, 136eqeltrid 2837 . . . . . . . . . . 11 (πœ‘ β†’ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
138134, 137eqeltrid 2837 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘‘)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
13998, 5, 133, 5, 138, 52cnmpt21 23182 . . . . . . . . 9 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (1st β€˜π‘§)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐽))
140132, 139eqeltrid 2837 . . . . . . . 8 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (1st β€˜(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐽))
141 fveq2 6891 . . . . . . . 8 (π‘₯ = (1st β€˜(2nd β€˜π‘€)) β†’ ((1st β€˜π‘€)β€˜π‘₯) = ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€))))
142108, 2, 113, 34, 131, 140, 141cnmptk1p 23196 . . . . . . 7 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ ((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐿 ↑ko 𝐾)))
143125, 142eqeltrrd 2834 . . . . . 6 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (𝑦 ∈ π‘Œ ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn (𝐿 ↑ko 𝐾)))
144104mpompt 7524 . . . . . . 7 (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (2nd β€˜(2nd β€˜π‘€))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§))
14561cbvmptv 5261 . . . . . . . . 9 (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘‘)) = (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§))
14685mpompt 7524 . . . . . . . . . 10 (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦)
1472, 3cnmpt2nd 23180 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
148146, 147eqeltrid 2837 . . . . . . . . 9 (πœ‘ β†’ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
149145, 148eqeltrid 2837 . . . . . . . 8 (πœ‘ β†’ (𝑑 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘‘)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
15098, 5, 133, 5, 149, 61cnmpt21 23182 . . . . . . 7 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ (2nd β€˜π‘§)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐾))
151144, 150eqeltrid 2837 . . . . . 6 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (2nd β€˜(2nd β€˜π‘€))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐾))
152 fveq2 6891 . . . . . 6 (𝑦 = (2nd β€˜(2nd β€˜π‘€)) β†’ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜π‘¦) = (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€))))
153108, 3, 33, 35, 143, 151, 152cnmptk1p 23196 . . . . 5 (πœ‘ β†’ (𝑀 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) Γ— (𝑋 Γ— π‘Œ)) ↦ (((1st β€˜π‘€)β€˜(1st β€˜(2nd β€˜π‘€)))β€˜(2nd β€˜(2nd β€˜π‘€)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐿))
154106, 153eqeltrrid 2838 . . . 4 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) Γ—t (𝐽 Γ—t 𝐾)) Cn 𝐿))
15598, 5, 154cnmpt2k 23199 . . 3 (πœ‘ β†’ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 Γ— π‘Œ) ↦ ((π‘”β€˜(1st β€˜π‘§))β€˜(2nd β€˜π‘§)))) ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
15689, 155eqeltrd 2833 . 2 (πœ‘ β†’ ◑𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾))))
157 ishmeo 23270 . 2 (𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ↔ (𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ∧ ◑𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 Γ—t 𝐾)))))
15881, 156, 157sylanbrc 583 1 (πœ‘ β†’ 𝐹 ∈ ((𝐿 ↑ko (𝐽 Γ—t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βŸ¨cop 4634  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  1st c1st 7975  2nd c2nd 7976  Topctop 22402  TopOnctopon 22419   Cn ccn 22735  Compccmp 22897  π‘›-Locally cnlly 22976   Γ—t ctx 23071   ↑ko cxko 23072  Homeochmeo 23264
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-rest 17370  df-topgen 17391  df-pt 17392  df-top 22403  df-topon 22420  df-bases 22456  df-ntr 22531  df-nei 22609  df-cn 22738  df-cnp 22739  df-cmp 22898  df-nlly 22978  df-tx 23073  df-xko 23074  df-hmeo 23266
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator