| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xkohmeo.f | . . 3
⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) | 
| 2 |  | xkohmeo.x | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 3 |  | xkohmeo.y | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 4 |  | txtopon 23600 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 5 | 2, 3, 4 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 6 |  | topontop 22920 | . . . . . 6
⊢ ((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝐽 ×t 𝐾) ∈ Top) | 
| 7 | 5, 6 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ Top) | 
| 8 |  | xkohmeo.l | . . . . 5
⊢ (𝜑 → 𝐿 ∈ Top) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢ (𝐿 ↑ko (𝐽 ×t 𝐾)) = (𝐿 ↑ko (𝐽 ×t 𝐾)) | 
| 10 | 9 | xkotopon 23609 | . . . . 5
⊢ (((𝐽 ×t 𝐾) ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko (𝐽 ×t 𝐾)) ∈ (TopOn‘((𝐽 ×t 𝐾) Cn 𝐿))) | 
| 11 | 7, 8, 10 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐿 ↑ko (𝐽 ×t 𝐾)) ∈ (TopOn‘((𝐽 ×t 𝐾) Cn 𝐿))) | 
| 12 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑓 ∈ V | 
| 13 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 14 | 12, 13 | op1std 8025 | . . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑥〉 → (1st ‘𝑧) = 𝑓) | 
| 15 | 12, 13 | op2ndd 8026 | . . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑥〉 → (2nd ‘𝑧) = 𝑥) | 
| 16 |  | eqidd 2737 | . . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑥〉 → 𝑦 = 𝑦) | 
| 17 | 14, 15, 16 | oveq123d 7453 | . . . . . . 7
⊢ (𝑧 = 〈𝑓, 𝑥〉 → ((2nd ‘𝑧)(1st ‘𝑧)𝑦) = (𝑥𝑓𝑦)) | 
| 18 | 17 | mpteq2dv 5243 | . . . . . 6
⊢ (𝑧 = 〈𝑓, 𝑥〉 → (𝑦 ∈ 𝑌 ↦ ((2nd ‘𝑧)(1st ‘𝑧)𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) | 
| 19 | 18 | mpompt 7548 | . . . . 5
⊢ (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (𝑦 ∈ 𝑌 ↦ ((2nd ‘𝑧)(1st ‘𝑧)𝑦))) = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) | 
| 20 |  | txtopon 23600 | . . . . . . 7
⊢ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ∈ (TopOn‘((𝐽 ×t 𝐾) Cn 𝐿)) ∧ 𝐽 ∈ (TopOn‘𝑋)) → ((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ∈ (TopOn‘(((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋))) | 
| 21 | 11, 2, 20 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ∈ (TopOn‘(((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋))) | 
| 22 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 23 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 24 | 22, 23 | op1std 8025 | . . . . . . . . . 10
⊢ (𝑤 = 〈𝑧, 𝑦〉 → (1st ‘𝑤) = 𝑧) | 
| 25 | 24 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑧, 𝑦〉 → (1st
‘(1st ‘𝑤)) = (1st ‘𝑧)) | 
| 26 | 24 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑧, 𝑦〉 → (2nd
‘(1st ‘𝑤)) = (2nd ‘𝑧)) | 
| 27 | 22, 23 | op2ndd 8026 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑧, 𝑦〉 → (2nd ‘𝑤) = 𝑦) | 
| 28 | 25, 26, 27 | oveq123d 7453 | . . . . . . . 8
⊢ (𝑤 = 〈𝑧, 𝑦〉 → ((2nd
‘(1st ‘𝑤))(1st ‘(1st
‘𝑤))(2nd
‘𝑤)) =
((2nd ‘𝑧)(1st ‘𝑧)𝑦)) | 
| 29 | 28 | mpompt 7548 | . . . . . . 7
⊢ (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ ((2nd
‘(1st ‘𝑤))(1st ‘(1st
‘𝑤))(2nd
‘𝑤))) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ ((2nd ‘𝑧)(1st ‘𝑧)𝑦)) | 
| 30 |  | txtopon 23600 | . . . . . . . . 9
⊢ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ∈ (TopOn‘(((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋)) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) ∈ (TopOn‘((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌))) | 
| 31 | 21, 3, 30 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) ∈ (TopOn‘((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌))) | 
| 32 |  | toptopon2 22925 | . . . . . . . . 9
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 33 | 8, 32 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 34 |  | xkohmeo.j | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ 𝑛-Locally
Comp) | 
| 35 |  | xkohmeo.k | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
Comp) | 
| 36 |  | txcmp 23652 | . . . . . . . . . 10
⊢ ((𝑥 ∈ Comp ∧ 𝑦 ∈ Comp) → (𝑥 ×t 𝑦) ∈ Comp) | 
| 37 | 36 | txnlly 23646 | . . . . . . . . 9
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐾 ∈
𝑛-Locally Comp) → (𝐽 ×t 𝐾) ∈ 𝑛-Locally
Comp) | 
| 38 | 34, 35, 37 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ 𝑛-Locally
Comp) | 
| 39 | 25 | mpompt 7548 | . . . . . . . . . 10
⊢ (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (1st
‘(1st ‘𝑤))) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ (1st ‘𝑧)) | 
| 40 | 5 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 41 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 42 |  | xp1st 8047 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) → (1st ‘𝑤) ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋)) | 
| 43 | 42 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → (1st ‘𝑤) ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋)) | 
| 44 |  | xp1st 8047 | . . . . . . . . . . . . . 14
⊢
((1st ‘𝑤) ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) → (1st
‘(1st ‘𝑤)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → (1st
‘(1st ‘𝑤)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) | 
| 46 |  | cnf2 23258 | . . . . . . . . . . . . 13
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (1st ‘(1st ‘𝑤)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (1st
‘(1st ‘𝑤)):(𝑋 × 𝑌)⟶∪ 𝐿) | 
| 47 | 40, 41, 45, 46 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → (1st
‘(1st ‘𝑤)):(𝑋 × 𝑌)⟶∪ 𝐿) | 
| 48 | 47 | feqmptd 6976 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌)) → (1st
‘(1st ‘𝑤)) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ((1st
‘(1st ‘𝑤))‘𝑢))) | 
| 49 | 48 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (1st
‘(1st ‘𝑤))) = (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (𝑢 ∈ (𝑋 × 𝑌) ↦ ((1st
‘(1st ‘𝑤))‘𝑢)))) | 
| 50 | 39, 49 | eqtr3id 2790 | . . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ (1st ‘𝑧)) = (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (𝑢 ∈ (𝑋 × 𝑌) ↦ ((1st
‘(1st ‘𝑤))‘𝑢)))) | 
| 51 | 21, 3 | cnmpt1st 23677 | . . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ 𝑧) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn ((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽))) | 
| 52 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → (1st ‘𝑡) = (1st ‘𝑧)) | 
| 53 | 52 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑡 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (1st ‘𝑡)) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (1st ‘𝑧)) | 
| 54 | 14 | mpompt 7548 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (1st ‘𝑧)) = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ 𝑓) | 
| 55 | 11, 2 | cnmpt1st 23677 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ 𝑓) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 56 | 54, 55 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (1st ‘𝑧)) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 57 | 53, 56 | eqeltrid 2844 | . . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (1st ‘𝑡)) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 58 | 21, 3, 51, 21, 57, 52 | cnmpt21 23680 | . . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ (1st ‘𝑧)) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 59 | 50, 58 | eqeltrrd 2841 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (𝑢 ∈ (𝑋 × 𝑌) ↦ ((1st
‘(1st ‘𝑤))‘𝑢))) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 60 | 26 | mpompt 7548 | . . . . . . . . . 10
⊢ (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (2nd
‘(1st ‘𝑤))) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ (2nd ‘𝑧)) | 
| 61 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) | 
| 62 | 61 | cbvmptv 5254 | . . . . . . . . . . . 12
⊢ (𝑡 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (2nd ‘𝑡)) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (2nd ‘𝑧)) | 
| 63 | 15 | mpompt 7548 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (2nd ‘𝑧)) = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ 𝑥) | 
| 64 | 11, 2 | cnmpt2nd 23678 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn 𝐽)) | 
| 65 | 63, 64 | eqeltrid 2844 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (2nd ‘𝑧)) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn 𝐽)) | 
| 66 | 62, 65 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (2nd ‘𝑡)) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn 𝐽)) | 
| 67 | 21, 3, 51, 21, 66, 61 | cnmpt21 23680 | . . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ (2nd ‘𝑧)) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn 𝐽)) | 
| 68 | 60, 67 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (2nd
‘(1st ‘𝑤))) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn 𝐽)) | 
| 69 | 27 | mpompt 7548 | . . . . . . . . . 10
⊢ (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (2nd ‘𝑤)) = (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ 𝑦) | 
| 70 | 21, 3 | cnmpt2nd 23678 | . . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn 𝐾)) | 
| 71 | 69, 70 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ (2nd ‘𝑤)) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn 𝐾)) | 
| 72 | 31, 68, 71 | cnmpt1t 23674 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ 〈(2nd
‘(1st ‘𝑤)), (2nd ‘𝑤)〉) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn (𝐽 ×t 𝐾))) | 
| 73 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑢 = 〈(2nd
‘(1st ‘𝑤)), (2nd ‘𝑤)〉 → ((1st
‘(1st ‘𝑤))‘𝑢) = ((1st ‘(1st
‘𝑤))‘〈(2nd
‘(1st ‘𝑤)), (2nd ‘𝑤)〉)) | 
| 74 |  | df-ov 7435 | . . . . . . . . 9
⊢
((2nd ‘(1st ‘𝑤))(1st ‘(1st
‘𝑤))(2nd
‘𝑤)) =
((1st ‘(1st ‘𝑤))‘〈(2nd
‘(1st ‘𝑤)), (2nd ‘𝑤)〉) | 
| 75 | 73, 74 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑢 = 〈(2nd
‘(1st ‘𝑤)), (2nd ‘𝑤)〉 → ((1st
‘(1st ‘𝑤))‘𝑢) = ((2nd ‘(1st
‘𝑤))(1st
‘(1st ‘𝑤))(2nd ‘𝑤))) | 
| 76 | 31, 5, 33, 38, 59, 72, 75 | cnmptk1p 23694 | . . . . . . 7
⊢ (𝜑 → (𝑤 ∈ ((((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) × 𝑌) ↦ ((2nd
‘(1st ‘𝑤))(1st ‘(1st
‘𝑤))(2nd
‘𝑤))) ∈
((((𝐿 ↑ko
(𝐽 ×t
𝐾)) ×t
𝐽) ×t
𝐾) Cn 𝐿)) | 
| 77 | 29, 76 | eqeltrrid 2845 | . . . . . 6
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋), 𝑦 ∈ 𝑌 ↦ ((2nd ‘𝑧)(1st ‘𝑧)𝑦)) ∈ ((((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) ×t 𝐾) Cn 𝐿)) | 
| 78 | 21, 3, 77 | cnmpt2k 23697 | . . . . 5
⊢ (𝜑 → (𝑧 ∈ (((𝐽 ×t 𝐾) Cn 𝐿) × 𝑋) ↦ (𝑦 ∈ 𝑌 ↦ ((2nd ‘𝑧)(1st ‘𝑧)𝑦))) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn (𝐿 ↑ko 𝐾))) | 
| 79 | 19, 78 | eqeltrrid 2845 | . . . 4
⊢ (𝜑 → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿), 𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (((𝐿 ↑ko (𝐽 ×t 𝐾)) ×t 𝐽) Cn (𝐿 ↑ko 𝐾))) | 
| 80 | 11, 2, 79 | cnmpt2k 23697 | . . 3
⊢ (𝜑 → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽))) | 
| 81 | 1, 80 | eqeltrid 2844 | . 2
⊢ (𝜑 → 𝐹 ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽))) | 
| 82 | 2, 3, 1, 34, 35, 8 | xkocnv 23823 | . . . 4
⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) | 
| 83 | 13, 23 | op1std 8025 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) | 
| 84 | 83 | fveq2d 6909 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑔‘(1st ‘𝑧)) = (𝑔‘𝑥)) | 
| 85 | 13, 23 | op2ndd 8026 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) | 
| 86 | 84, 85 | fveq12d 6912 | . . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧)) = ((𝑔‘𝑥)‘𝑦)) | 
| 87 | 86 | mpompt 7548 | . . . . 5
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) | 
| 88 | 87 | mpteq2i 5246 | . . . 4
⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) | 
| 89 | 82, 88 | eqtr4di 2794 | . . 3
⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧))))) | 
| 90 |  | nllytop 23482 | . . . . . 6
⊢ (𝐽 ∈ 𝑛-Locally Comp
→ 𝐽 ∈
Top) | 
| 91 | 34, 90 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 92 |  | nllytop 23482 | . . . . . . 7
⊢ (𝐾 ∈ 𝑛-Locally Comp
→ 𝐾 ∈
Top) | 
| 93 | 35, 92 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 94 |  | xkotop 23597 | . . . . . 6
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ Top) | 
| 95 | 93, 8, 94 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ Top) | 
| 96 |  | eqid 2736 | . . . . . 6
⊢ ((𝐿 ↑ko 𝐾) ↑ko 𝐽) = ((𝐿 ↑ko 𝐾) ↑ko 𝐽) | 
| 97 | 96 | xkotopon 23609 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝐿 ↑ko 𝐾) ∈ Top) → ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOn‘(𝐽 Cn (𝐿 ↑ko 𝐾)))) | 
| 98 | 91, 95, 97 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOn‘(𝐽 Cn (𝐿 ↑ko 𝐾)))) | 
| 99 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑔 ∈ V | 
| 100 | 99, 22 | op1std 8025 | . . . . . . . 8
⊢ (𝑤 = 〈𝑔, 𝑧〉 → (1st ‘𝑤) = 𝑔) | 
| 101 | 99, 22 | op2ndd 8026 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑔, 𝑧〉 → (2nd ‘𝑤) = 𝑧) | 
| 102 | 101 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = 〈𝑔, 𝑧〉 → (1st
‘(2nd ‘𝑤)) = (1st ‘𝑧)) | 
| 103 | 100, 102 | fveq12d 6912 | . . . . . . 7
⊢ (𝑤 = 〈𝑔, 𝑧〉 → ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))) = (𝑔‘(1st ‘𝑧))) | 
| 104 | 101 | fveq2d 6909 | . . . . . . 7
⊢ (𝑤 = 〈𝑔, 𝑧〉 → (2nd
‘(2nd ‘𝑤)) = (2nd ‘𝑧)) | 
| 105 | 103, 104 | fveq12d 6912 | . . . . . 6
⊢ (𝑤 = 〈𝑔, 𝑧〉 → (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘(2nd
‘(2nd ‘𝑤))) = ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧))) | 
| 106 | 105 | mpompt 7548 | . . . . 5
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘(2nd
‘(2nd ‘𝑤)))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧))) | 
| 107 |  | txtopon 23600 | . . . . . . 7
⊢ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ∈ (TopOn‘(𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) → (((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) ∈ (TopOn‘((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)))) | 
| 108 | 98, 5, 107 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) ∈ (TopOn‘((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)))) | 
| 109 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → 𝐾 ∈ (TopOn‘𝑌)) | 
| 110 | 33 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 111 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) | 
| 112 | 111 | xkotopon 23609 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 113 | 93, 8, 112 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 114 |  | xp1st 8047 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) → (1st ‘𝑤) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) | 
| 115 |  | cnf2 23258 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (1st ‘𝑤) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (1st ‘𝑤):𝑋⟶(𝐾 Cn 𝐿)) | 
| 116 | 2, 113, 114, 115 | syl2an3an 1423 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → (1st ‘𝑤):𝑋⟶(𝐾 Cn 𝐿)) | 
| 117 |  | xp2nd 8048 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) → (2nd ‘𝑤) ∈ (𝑋 × 𝑌)) | 
| 118 | 117 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → (2nd ‘𝑤) ∈ (𝑋 × 𝑌)) | 
| 119 |  | xp1st 8047 | . . . . . . . . . . . 12
⊢
((2nd ‘𝑤) ∈ (𝑋 × 𝑌) → (1st
‘(2nd ‘𝑤)) ∈ 𝑋) | 
| 120 | 118, 119 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → (1st
‘(2nd ‘𝑤)) ∈ 𝑋) | 
| 121 | 116, 120 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))) ∈ (𝐾 Cn 𝐿)) | 
| 122 |  | cnf2 23258 | . . . . . . . . . 10
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))) ∈ (𝐾 Cn 𝐿)) → ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))):𝑌⟶∪ 𝐿) | 
| 123 | 109, 110,
121, 122 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))):𝑌⟶∪ 𝐿) | 
| 124 | 123 | feqmptd 6976 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤))) = (𝑦 ∈ 𝑌 ↦ (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘𝑦))) | 
| 125 | 124 | mpteq2dva 5241 | . . . . . . 7
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))) = (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (𝑦 ∈ 𝑌 ↦ (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘𝑦)))) | 
| 126 | 100 | mpompt 7548 | . . . . . . . . . 10
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (1st ‘𝑤)) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ 𝑔) | 
| 127 | 116 | feqmptd 6976 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌))) → (1st ‘𝑤) = (𝑥 ∈ 𝑋 ↦ ((1st ‘𝑤)‘𝑥))) | 
| 128 | 127 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (1st ‘𝑤)) = (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (𝑥 ∈ 𝑋 ↦ ((1st ‘𝑤)‘𝑥)))) | 
| 129 | 126, 128 | eqtr3id 2790 | . . . . . . . . 9
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ 𝑔) = (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (𝑥 ∈ 𝑋 ↦ ((1st ‘𝑤)‘𝑥)))) | 
| 130 | 98, 5 | cnmpt1st 23677 | . . . . . . . . 9
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ 𝑔) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽))) | 
| 131 | 129, 130 | eqeltrrd 2841 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (𝑥 ∈ 𝑋 ↦ ((1st ‘𝑤)‘𝑥))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽))) | 
| 132 | 102 | mpompt 7548 | . . . . . . . . 9
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (1st
‘(2nd ‘𝑤))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) | 
| 133 | 98, 5 | cnmpt2nd 23678 | . . . . . . . . . 10
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ 𝑧) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn (𝐽 ×t 𝐾))) | 
| 134 | 52 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑡)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) | 
| 135 | 83 | mpompt 7548 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) | 
| 136 | 2, 3 | cnmpt1st 23677 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | 
| 137 | 135, 136 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | 
| 138 | 134, 137 | eqeltrid 2844 | . . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑡)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | 
| 139 | 98, 5, 133, 5, 138, 52 | cnmpt21 23680 | . . . . . . . . 9
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn 𝐽)) | 
| 140 | 132, 139 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (1st
‘(2nd ‘𝑤))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn 𝐽)) | 
| 141 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = (1st
‘(2nd ‘𝑤)) → ((1st ‘𝑤)‘𝑥) = ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))) | 
| 142 | 108, 2, 113, 34, 131, 140, 141 | cnmptk1p 23694 | . . . . . . 7
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ ((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn (𝐿 ↑ko 𝐾))) | 
| 143 | 125, 142 | eqeltrrd 2841 | . . . . . 6
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (𝑦 ∈ 𝑌 ↦ (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘𝑦))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn (𝐿 ↑ko 𝐾))) | 
| 144 | 104 | mpompt 7548 | . . . . . . 7
⊢ (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (2nd
‘(2nd ‘𝑤))) = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) | 
| 145 | 61 | cbvmptv 5254 | . . . . . . . . 9
⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑡)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) | 
| 146 | 85 | mpompt 7548 | . . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) | 
| 147 | 2, 3 | cnmpt2nd 23678 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 148 | 146, 147 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 149 | 145, 148 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑡)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 150 | 98, 5, 133, 5, 149, 61 | cnmpt21 23680 | . . . . . . 7
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn 𝐾)) | 
| 151 | 144, 150 | eqeltrid 2844 | . . . . . 6
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (2nd
‘(2nd ‘𝑤))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn 𝐾)) | 
| 152 |  | fveq2 6905 | . . . . . 6
⊢ (𝑦 = (2nd
‘(2nd ‘𝑤)) → (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘𝑦) = (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘(2nd
‘(2nd ‘𝑤)))) | 
| 153 | 108, 3, 33, 35, 143, 151, 152 | cnmptk1p 23694 | . . . . 5
⊢ (𝜑 → (𝑤 ∈ ((𝐽 Cn (𝐿 ↑ko 𝐾)) × (𝑋 × 𝑌)) ↦ (((1st ‘𝑤)‘(1st
‘(2nd ‘𝑤)))‘(2nd
‘(2nd ‘𝑤)))) ∈ ((((𝐿 ↑ko 𝐾) ↑ko 𝐽) ×t (𝐽 ×t 𝐾)) Cn 𝐿)) | 
| 154 | 106, 153 | eqeltrrid 2845 | . . . 4
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)), 𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧))) ∈
((((𝐿 ↑ko
𝐾) ↑ko
𝐽) ×t
(𝐽 ×t
𝐾)) Cn 𝐿)) | 
| 155 | 98, 5, 154 | cnmpt2k 23697 | . . 3
⊢ (𝜑 → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((𝑔‘(1st ‘𝑧))‘(2nd
‘𝑧)))) ∈
(((𝐿 ↑ko
𝐾) ↑ko
𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 156 | 89, 155 | eqeltrd 2840 | . 2
⊢ (𝜑 → ◡𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾)))) | 
| 157 |  | ishmeo 23768 | . 2
⊢ (𝐹 ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ↔ (𝐹 ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾)) Cn ((𝐿 ↑ko 𝐾) ↑ko 𝐽)) ∧ ◡𝐹 ∈ (((𝐿 ↑ko 𝐾) ↑ko 𝐽) Cn (𝐿 ↑ko (𝐽 ×t 𝐾))))) | 
| 158 | 81, 156, 157 | sylanbrc 583 | 1
⊢ (𝜑 → 𝐹 ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽))) |