Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
2 | | cnmptid.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | cnmpt11.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
4 | | cnmpt11.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
5 | | cnf2 21255 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
6 | 2, 3, 4, 5 | syl3anc 1477 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
7 | | eqid 2760 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
8 | 7 | fmpt 6544 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ 𝑌 ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) |
9 | 6, 8 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐴 ∈ 𝑌) |
10 | 9 | r19.21bi 3070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
11 | 7 | fvmpt2 6453 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
12 | 1, 10, 11 | syl2anc 696 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
13 | 12 | fveq2d 6356 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴)) |
14 | | cnmpt11.c |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → 𝐵 = 𝐶) |
15 | 14 | eleq1d 2824 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐵 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿)) |
16 | | cnmpt11.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) |
17 | | cntop2 21247 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿) → 𝐿 ∈ Top) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ Top) |
19 | | eqid 2760 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐿 =
∪ 𝐿 |
20 | 19 | toptopon 20924 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
21 | 18, 20 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
22 | | cnf2 21255 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
23 | 3, 21, 16, 22 | syl3anc 1477 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
24 | | eqid 2760 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑦 ∈ 𝑌 ↦ 𝐵) |
25 | 24 | fmpt 6544 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑌 𝐵 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿) |
26 | 23, 25 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
27 | 26 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿) |
28 | 15, 27, 10 | rspcdva 3455 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ∪ 𝐿) |
29 | 14, 24 | fvmptg 6442 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑌 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴) = 𝐶) |
30 | 10, 28, 29 | syl2anc 696 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘𝐴) = 𝐶) |
31 | 13, 30 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) = 𝐶) |
32 | | fvco3 6437 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
33 | 6, 32 | sylan 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑦 ∈ 𝑌 ↦ 𝐵)‘((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥))) |
34 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 ↦ 𝐶) = (𝑥 ∈ 𝑋 ↦ 𝐶) |
35 | 34 | fvmpt2 6453 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
36 | 1, 28, 35 | syl2anc 696 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = 𝐶) |
37 | 31, 33, 36 | 3eqtr4d 2804 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
38 | 37 | ralrimiva 3104 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥)) |
39 | | nfv 1992 |
. . . . 5
⊢
Ⅎ𝑧(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) |
40 | | nfcv 2902 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑦 ∈ 𝑌 ↦ 𝐵) |
41 | | nfmpt1 4899 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐴) |
42 | 40, 41 | nfco 5443 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) |
43 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
44 | 42, 43 | nffv 6359 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) |
45 | | nfmpt1 4899 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 𝐶) |
46 | 45, 43 | nffv 6359 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
47 | 44, 46 | nfeq 2914 |
. . . . 5
⊢
Ⅎ𝑥(((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧) |
48 | | fveq2 6352 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧)) |
49 | | fveq2 6352 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
50 | 48, 49 | eqeq12d 2775 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
51 | 39, 47, 50 | cbvral 3306 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑥) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
52 | 38, 51 | sylib 208 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧)) |
53 | | fco 6219 |
. . . . . 6
⊢ (((𝑦 ∈ 𝑌 ↦ 𝐵):𝑌⟶∪ 𝐿 ∧ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶𝑌) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
54 | 23, 6, 53 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿) |
55 | | ffn 6206 |
. . . . 5
⊢ (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)):𝑋⟶∪ 𝐿 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋) |
56 | 54, 55 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋) |
57 | 28, 34 | fmptd 6548 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶):𝑋⟶∪ 𝐿) |
58 | | ffn 6206 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐶):𝑋⟶∪ 𝐿 → (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) |
59 | 57, 58 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) |
60 | | eqfnfv 6474 |
. . . 4
⊢ ((((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) Fn 𝑋 ∧ (𝑥 ∈ 𝑋 ↦ 𝐶) Fn 𝑋) → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
61 | 56, 59, 60 | syl2anc 696 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶) ↔ ∀𝑧 ∈ 𝑋 (((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑧) = ((𝑥 ∈ 𝑋 ↦ 𝐶)‘𝑧))) |
62 | 52, 61 | mpbird 247 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) |
63 | | cnco 21272 |
. . 3
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
64 | 4, 16, 63 | syl2anc 696 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝑌 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋 ↦ 𝐴)) ∈ (𝐽 Cn 𝐿)) |
65 | 62, 64 | eqeltrrd 2840 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |