Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
2 | | cnmptid.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | cnmpt11.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
4 | | cnmpt11.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
5 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
6 | 2, 3, 4, 5 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
7 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
8 | 7 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ 𝑌 ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
9 | 6, 8 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐴 ∈ 𝑌) |
10 | 9 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
11 | 7 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
12 | 1, 10, 11 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
13 | 12 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴)) |
14 | | cnmpt11.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) |
15 | | cntop2 20855 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿) → 𝐿 ∈ Top) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ Top) |
17 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐿 =
∪ 𝐿 |
18 | 17 | toptopon 20548 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
19 | 16, 18 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
20 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
21 | 3, 19, 14, 20 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
22 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑦 ∈ 𝑌 ↦ 𝐵) |
23 | 22 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑌 𝐵 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
24 | 21, 23 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
26 | | cnmpt11.c |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → 𝐵 = 𝐶) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝐵 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿)) |
28 | 27 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑌 → (∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿 → 𝐶 ∈ ∪ 𝐿)) |
29 | 10, 25, 28 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ∪ 𝐿) |
30 | 26, 22 | fvmptg 6189 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑌 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴) = 𝐶) |
31 | 10, 29, 30 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴) = 𝐶) |
32 | 13, 31 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = 𝐶) |
33 | | fvco3 6185 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
34 | 6, 33 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
35 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 ↦ 𝐶) = (𝑥 ∈ 𝑋 ↦ 𝐶) |
36 | 35 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
37 | 1, 29, 36 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
38 | 32, 34, 37 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
39 | 38 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
40 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑧(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) |
41 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑦 ∈ 𝑌 ↦ 𝐵) |
42 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐴) |
43 | 41, 42 | nfco 5209 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) |
44 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
45 | 43, 44 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) |
46 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐶) |
47 | 46, 44 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
48 | 45, 47 | nfeq 2762 |
. . . . 5
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
49 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧)) |
50 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
51 | 49, 50 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
52 | 40, 48, 51 | cbvral 3143 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
53 | 39, 52 | sylib 207 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
54 | | fco 5971 |
. . . . . 6
⊢ (((𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿 ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
55 | 21, 6, 54 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
56 | | ffn 5958 |
. . . . 5
⊢ (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋) |
58 | 29, 35 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶):𝑋⟶∪ 𝐿) |
59 | | ffn 5958 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐶):𝑋⟶∪ 𝐿 → (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) |
60 | 58, 59 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) |
61 | | eqfnfv 6219 |
. . . 4
⊢ ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋 ∧ (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
62 | 57, 60, 61 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
63 | 53, 62 | mpbird 246 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) |
64 | | cnco 20880 |
. . 3
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
65 | 4, 14, 64 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
66 | 63, 65 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |