| Step | Hyp | Ref
| Expression |
| 1 | | cidfval.i |
. 2
⊢ 1 =
(Id‘𝐶) |
| 2 | | cidfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 3 | | fvexd 6921 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) ∈ V) |
| 4 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
| 5 | | cidfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
| 6 | 4, 5 | eqtr4di 2795 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
| 7 | | fvexd 6921 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V) |
| 8 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
| 10 | | cidfval.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
| 12 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) ∈ V) |
| 13 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → 𝑐 = 𝐶) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = (comp‘𝐶)) |
| 15 | | cidfval.o |
. . . . . . . 8
⊢ · =
(comp‘𝐶) |
| 16 | 14, 15 | eqtr4di 2795 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = · ) |
| 17 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵) |
| 18 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ℎ = 𝐻) |
| 19 | 18 | oveqd 7448 |
. . . . . . . . 9
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥ℎ𝑥) = (𝑥𝐻𝑥)) |
| 20 | 18 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑦ℎ𝑥) = (𝑦𝐻𝑥)) |
| 21 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · ) |
| 22 | 21 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(〈𝑦, 𝑥〉𝑜𝑥) = (〈𝑦, 𝑥〉 · 𝑥)) |
| 23 | 22 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓)) |
| 24 | 23 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
| 25 | 20, 24 | raleqbidv 3346 |
. . . . . . . . . . 11
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
| 26 | 18 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥ℎ𝑦) = (𝑥𝐻𝑦)) |
| 27 | 21 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(〈𝑥, 𝑥〉𝑜𝑦) = (〈𝑥, 𝑥〉 · 𝑦)) |
| 28 | 27 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔)) |
| 29 | 28 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
| 30 | 26, 29 | raleqbidv 3346 |
. . . . . . . . . . 11
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
| 31 | 25, 30 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
((∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
| 32 | 17, 31 | raleqbidv 3346 |
. . . . . . . . 9
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
| 33 | 19, 32 | riotaeqbidv 7391 |
. . . . . . . 8
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(℩𝑔 ∈
(𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
| 34 | 17, 33 | mpteq12dv 5233 |
. . . . . . 7
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 35 | 12, 16, 34 | csbied2 3936 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 36 | 7, 11, 35 | csbied2 3936 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 37 | 3, 6, 36 | csbied2 3936 |
. . . 4
⊢ (𝑐 = 𝐶 → ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 38 | | df-cid 17712 |
. . . 4
⊢ Id =
(𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) |
| 39 | 37, 38, 5 | mptfvmpt 7248 |
. . 3
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 40 | 2, 39 | syl 17 |
. 2
⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
| 41 | 1, 40 | eqtrid 2789 |
1
⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |