Step | Hyp | Ref
| Expression |
1 | | cidfval.i |
. 2
⊢ 1 =
(Id‘𝐶) |
2 | | cidfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑐)
∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) ∈ V) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
6 | | cidfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵) |
8 | | fvex 6113 |
. . . . . . 7
⊢ (Hom
‘𝑐) ∈
V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V) |
10 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
11 | 10 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
12 | | cidfval.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
14 | | fvex 6113 |
. . . . . . . 8
⊢
(comp‘𝑐)
∈ V |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) ∈ V) |
16 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → 𝑐 = 𝐶) |
17 | 16 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = (comp‘𝐶)) |
18 | | cidfval.o |
. . . . . . . 8
⊢ · =
(comp‘𝐶) |
19 | 17, 18 | syl6eqr 2662 |
. . . . . . 7
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → (comp‘𝑐) = · ) |
20 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵) |
21 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ℎ = 𝐻) |
22 | 21 | oveqd 6566 |
. . . . . . . . 9
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥ℎ𝑥) = (𝑥𝐻𝑥)) |
23 | 21 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑦ℎ𝑥) = (𝑦𝐻𝑥)) |
24 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · ) |
25 | 24 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(〈𝑦, 𝑥〉𝑜𝑥) = (〈𝑦, 𝑥〉 · 𝑥)) |
26 | 25 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓)) |
27 | 26 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
28 | 23, 27 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
29 | 21 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥ℎ𝑦) = (𝑥𝐻𝑦)) |
30 | 24 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(〈𝑥, 𝑥〉𝑜𝑦) = (〈𝑥, 𝑥〉 · 𝑦)) |
31 | 30 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
33 | 29, 32 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
34 | 28, 33 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
((∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
35 | 20, 34 | raleqbidv 3129 |
. . . . . . . . 9
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
36 | 22, 35 | riotaeqbidv 6514 |
. . . . . . . 8
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) →
(℩𝑔 ∈
(𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) |
37 | 20, 36 | mpteq12dv 4663 |
. . . . . . 7
⊢ ((((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) ∧ 𝑜 = · ) → (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
38 | 15, 19, 37 | csbied2 3527 |
. . . . . 6
⊢ (((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐻) → ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
39 | 9, 13, 38 | csbied2 3527 |
. . . . 5
⊢ ((𝑐 = 𝐶 ∧ 𝑏 = 𝐵) → ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
40 | 4, 7, 39 | csbied2 3527 |
. . . 4
⊢ (𝑐 = 𝐶 → ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
41 | | df-cid 16153 |
. . . 4
⊢ Id =
(𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) |
42 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
43 | 6, 42 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
44 | 43 | mptex 6390 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓))) ∈ V |
45 | 40, 41, 44 | fvmpt 6191 |
. . 3
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
46 | 2, 45 | syl 17 |
. 2
⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
47 | 1, 46 | syl5eq 2656 |
1
⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |