Step | Hyp | Ref
| Expression |
1 | | comfffval.o |
. 2
⊢ 𝑂 =
(compf‘𝐶) |
2 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
3 | | comfffval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
5 | 4 | sqxpeqd 5065 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((Base‘𝑐) × (Base‘𝑐)) = (𝐵 × 𝐵)) |
6 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (Hom ‘𝑐) = (Hom ‘𝐶)) |
7 | | comfffval.h |
. . . . . . . 8
⊢ 𝐻 = (Hom ‘𝐶) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Hom ‘𝑐) = 𝐻) |
9 | 8 | oveqd 6566 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((2nd ‘𝑥)(Hom ‘𝑐)𝑦) = ((2nd ‘𝑥)𝐻𝑦)) |
10 | 8 | fveq1d 6105 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((Hom ‘𝑐)‘𝑥) = (𝐻‘𝑥)) |
11 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (comp‘𝑐) = (comp‘𝐶)) |
12 | | comfffval.x |
. . . . . . . . 9
⊢ · =
(comp‘𝐶) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (comp‘𝑐) = · ) |
14 | 13 | oveqd 6566 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑥(comp‘𝑐)𝑦) = (𝑥 · 𝑦)) |
15 | 14 | oveqd 6566 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (𝑔(𝑥(comp‘𝑐)𝑦)𝑓) = (𝑔(𝑥 · 𝑦)𝑓)) |
16 | 9, 10, 15 | mpt2eq123dv 6615 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)) = (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |
17 | 5, 4, 16 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
18 | | df-comf 16155 |
. . . 4
⊢
compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))) |
19 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
20 | 3, 19 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
21 | 20, 20 | xpex 6860 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
22 | 21, 20 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) ∈ V |
23 | 17, 18, 22 | fvmpt 6191 |
. . 3
⊢ (𝐶 ∈ V →
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
24 | | fvprc 6097 |
. . . 4
⊢ (¬
𝐶 ∈ V →
(compf‘𝐶) = ∅) |
25 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝐶 ∈ V →
(Base‘𝐶) =
∅) |
26 | 3, 25 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝐶 ∈ V → 𝐵 = ∅) |
27 | 26 | xpeq2d 5063 |
. . . . . . 7
⊢ (¬
𝐶 ∈ V → (𝐵 × 𝐵) = (𝐵 × ∅)) |
28 | | xp0 5471 |
. . . . . . 7
⊢ (𝐵 × ∅) =
∅ |
29 | 27, 28 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝐶 ∈ V → (𝐵 × 𝐵) = ∅) |
30 | | mpt2eq12 6613 |
. . . . . 6
⊢ (((𝐵 × 𝐵) = ∅ ∧ 𝐵 = ∅) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
31 | 29, 26, 30 | syl2anc 691 |
. . . . 5
⊢ (¬
𝐶 ∈ V → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
32 | | mpt20 6623 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2nd
‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = ∅ |
33 | 31, 32 | syl6eq 2660 |
. . . 4
⊢ (¬
𝐶 ∈ V → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) = ∅) |
34 | 24, 33 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐶 ∈ V →
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))) |
35 | 23, 34 | pm2.61i 175 |
. 2
⊢
(compf‘𝐶) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |
36 | 1, 35 | eqtri 2632 |
1
⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) |