Step | Hyp | Ref
| Expression |
1 | | evlf1.e |
. . . 4
⊢ 𝐸 = (𝐶 evalF 𝐷) |
2 | | evlf1.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | evlf1.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
4 | | evlf1.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
5 | | eqid 2610 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | eqid 2610 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
7 | | eqid 2610 |
. . . 4
⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷) |
8 | 1, 2, 3, 4, 5, 6, 7 | evlfval 16680 |
. . 3
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) |
9 | | ovex 6577 |
. . . . 5
⊢ (𝐶 Func 𝐷) ∈ V |
10 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
11 | 4, 10 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
12 | 9, 11 | mpt2ex 7136 |
. . . 4
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V |
13 | 9, 11 | xpex 6860 |
. . . . 5
⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V |
14 | 13, 13 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V |
15 | 12, 14 | op1std 7069 |
. . 3
⊢ (𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉 → (1st
‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥))) |
16 | 8, 15 | syl 17 |
. 2
⊢ (𝜑 → (1st
‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥))) |
17 | | simprl 790 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝑋)) → 𝑓 = 𝐹) |
18 | 17 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝑋)) → (1st ‘𝑓) = (1st ‘𝐹)) |
19 | | simprr 792 |
. . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝑋)) → 𝑥 = 𝑋) |
20 | 18, 19 | fveq12d 6109 |
. 2
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝑋)) → ((1st ‘𝑓)‘𝑥) = ((1st ‘𝐹)‘𝑋)) |
21 | | evlf1.f |
. 2
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
22 | | evlf1.x |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
23 | | fvex 6113 |
. . 3
⊢
((1st ‘𝐹)‘𝑋) ∈ V |
24 | 23 | a1i 11 |
. 2
⊢ (𝜑 → ((1st
‘𝐹)‘𝑋) ∈ V) |
25 | 16, 20, 21, 22, 24 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) |