| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 2 | | cnmptid.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 3 | | cnmpt11.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
| 4 | | cnmpt11.a |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
| 5 | | cnf2 23257 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
| 6 | 2, 3, 4, 5 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
| 7 | 6 | fvmptelcdm 7133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
| 8 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
| 9 | 8 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
| 10 | 1, 7, 9 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
| 11 | 10 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴)) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑦 ∈ 𝑌 ↦ 𝐵) |
| 13 | | cnmpt11.c |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → 𝐵 = 𝐶) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐵 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿)) |
| 15 | | cnmpt11.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) |
| 16 | | cntop2 23249 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿) → 𝐿 ∈ Top) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ Top) |
| 18 | | toptopon2 22924 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
| 19 | 17, 18 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
| 20 | | cnf2 23257 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
| 21 | 3, 19, 15, 20 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
| 22 | 12 | fmpt 7130 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑌 𝐵 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
| 23 | 21, 22 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
| 25 | 14, 24, 7 | rspcdva 3623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ∪ 𝐿) |
| 26 | 12, 13, 7, 25 | fvmptd3 7039 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴) = 𝐶) |
| 27 | 11, 26 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = 𝐶) |
| 28 | | fvco3 7008 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
| 29 | 6, 28 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
| 30 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 ↦ 𝐶) = (𝑥 ∈ 𝑋 ↦ 𝐶) |
| 31 | 30 | fvmpt2 7027 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
| 32 | 1, 25, 31 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
| 33 | 27, 29, 32 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
| 34 | 33 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
| 35 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑧(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) |
| 36 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑦 ∈ 𝑌 ↦ 𝐵) |
| 37 | | nfmpt1 5250 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐴) |
| 38 | 36, 37 | nfco 5876 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) |
| 39 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
| 40 | 38, 39 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) |
| 41 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐶) |
| 42 | 41, 39 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
| 43 | 40, 42 | nfeq 2919 |
. . . . 5
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
| 44 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧)) |
| 45 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
| 46 | 44, 45 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
| 47 | 35, 43, 46 | cbvralw 3306 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
| 48 | 34, 47 | sylib 218 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
| 49 | | fco 6760 |
. . . . . 6
⊢ (((𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿 ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
| 50 | 21, 6, 49 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
| 51 | 50 | ffnd 6737 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋) |
| 52 | 25 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶):𝑋⟶∪ 𝐿) |
| 53 | 52 | ffnd 6737 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) |
| 54 | | eqfnfv 7051 |
. . . 4
⊢ ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋 ∧ (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
| 55 | 51, 53, 54 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
| 56 | 48, 55 | mpbird 257 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) |
| 57 | | cnco 23274 |
. . 3
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
| 58 | 4, 15, 57 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
| 59 | 56, 58 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |