Step | Hyp | Ref
| Expression |
1 | | comfffval.o |
. 2
⊢ 𝑂 =
(compf‘𝐶) |
2 | | fveq2 6768 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
3 | | comfffval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
4 | 2, 3 | eqtr4di 2797 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
5 | 4 | sqxpeqd 5620 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((Base‘𝑐) × (Base‘𝑐)) = (𝐵 × 𝐵)) |
6 | | fveq2 6768 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (Hom ‘𝑐) = (Hom ‘𝐶)) |
7 | | comfffval.h |
. . . . . . . 8
⊢ 𝐻 = (Hom ‘𝐶) |
8 | 6, 7 | eqtr4di 2797 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Hom ‘𝑐) = 𝐻) |
9 | 8 | oveqd 7285 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((2nd ‘𝑥)(Hom ‘𝑐)𝑦) = ((2nd ‘𝑥)𝐻𝑦)) |
10 | 8 | fveq1d 6770 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((Hom ‘𝑐)‘𝑥) = (𝐻‘𝑥)) |
11 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (comp‘𝑐) = (comp‘𝐶)) |
12 | | comfffval.x |
. . . . . . . . 9
⊢ · =
(comp‘𝐶) |
13 | 11, 12 | eqtr4di 2797 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (comp‘𝑐) = · ) |
14 | 13 | oveqd 7285 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑥(comp‘𝑐)𝑦) = (𝑥 · 𝑦)) |
15 | 14 | oveqd 7285 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (𝑔(𝑥(comp‘𝑐)𝑦)𝑓) = (𝑔(𝑥 · 𝑦)𝑓)) |
16 | 9, 10, 15 | mpoeq123dv 7341 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)) = (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |
17 | 5, 4, 16 | mpoeq123dv 7341 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
18 | | df-comf 17361 |
. . . 4
⊢
compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))) |
19 | 3 | fvexi 6782 |
. . . . . 6
⊢ 𝐵 ∈ V |
20 | 19, 19 | xpex 7594 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
21 | 20, 19 | mpoex 7906 |
. . . 4
⊢ (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) ∈ V |
22 | 17, 18, 21 | fvmpt 6869 |
. . 3
⊢ (𝐶 ∈ V →
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
23 | | fvprc 6760 |
. . . 4
⊢ (¬
𝐶 ∈ V →
(compf‘𝐶) = ∅) |
24 | | fvprc 6760 |
. . . . . . 7
⊢ (¬
𝐶 ∈ V →
(Base‘𝐶) =
∅) |
25 | 3, 24 | eqtrid 2791 |
. . . . . 6
⊢ (¬
𝐶 ∈ V → 𝐵 = ∅) |
26 | 25 | olcd 870 |
. . . . 5
⊢ (¬
𝐶 ∈ V → ((𝐵 × 𝐵) = ∅ ∨ 𝐵 = ∅)) |
27 | | 0mpo0 7349 |
. . . . 5
⊢ (((𝐵 × 𝐵) = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = ∅) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (¬
𝐶 ∈ V → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = ∅) |
29 | 23, 28 | eqtr4d 2782 |
. . 3
⊢ (¬
𝐶 ∈ V →
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
30 | 22, 29 | pm2.61i 182 |
. 2
⊢
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |
31 | 1, 30 | eqtri 2767 |
1
⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |