Step | Hyp | Ref
| Expression |
1 | | cnmptk1.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
2 | 1 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | cnmptk1.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
4 | 3 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍)) |
5 | | cnmptk1.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
6 | | topontop 21125 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
7 | 1, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Top) |
8 | | topontop 21125 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top) |
9 | 3, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Top) |
10 | | eqid 2777 |
. . . . . . . . . . 11
⊢ (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾) |
11 | 10 | xkotopon 21812 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
12 | 7, 9, 11 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
13 | | cnmptk1.a |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
14 | | cnf2 21461 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
15 | 5, 12, 13, 14 | syl3anc 1439 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
16 | | eqid 2777 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) |
17 | 16 | fmpt 6644 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿) ↔ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
18 | 15, 17 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
19 | 18 | r19.21bi 3113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
20 | | cnf2 21461 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
21 | 2, 4, 19, 20 | syl3anc 1439 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
22 | | eqid 2777 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) |
23 | 22 | fmpt 6644 |
. . . . 5
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
24 | 21, 23 | sylibr 226 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
25 | | eqidd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
26 | | eqidd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵)) |
27 | | cnmptk1.c |
. . . 4
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) |
28 | 24, 25, 26, 27 | fmptcof 6662 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑦 ∈ 𝑌 ↦ 𝐶)) |
29 | 28 | mpteq2dva 4979 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶))) |
30 | | cnmptk1.b |
. . . 4
⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) |
31 | 7, 30 | xkoco2cn 21870 |
. . 3
⊢ (𝜑 → (𝑤 ∈ (𝐾 Cn 𝐿) ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑤)) ∈ ((𝐿 ^ko 𝐾) Cn (𝑀 ^ko 𝐾))) |
32 | | coeq2 5526 |
. . 3
⊢ (𝑤 = (𝑦 ∈ 𝑌 ↦ 𝐴) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑤) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
33 | 5, 13, 12, 31, 32 | cnmpt11 21875 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) ∈ (𝐽 Cn (𝑀 ^ko 𝐾))) |
34 | 29, 33 | eqeltrrd 2859 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ^ko 𝐾))) |