Step | Hyp | Ref
| Expression |
1 | | cidfval.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | cidfval.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
3 | | cidfval.o |
. . 3
⊢ · =
(comp‘𝐶) |
4 | | cidfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
5 | | cidfval.i |
. . 3
⊢ 1 =
(Id‘𝐶) |
6 | 1, 2, 3, 4, 5 | cidfval 17385 |
. 2
⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) |
7 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
8 | 7, 7 | oveq12d 7293 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥𝐻𝑥) = (𝑋𝐻𝑋)) |
9 | 7 | oveq2d 7291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑦𝐻𝑥) = (𝑦𝐻𝑋)) |
10 | 7 | opeq2d 4811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 〈𝑦, 𝑥〉 = 〈𝑦, 𝑋〉) |
11 | 10, 7 | oveq12d 7293 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (〈𝑦, 𝑥〉 · 𝑥) = (〈𝑦, 𝑋〉 · 𝑋)) |
12 | 11 | oveqd 7292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = (𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓)) |
13 | 12 | eqeq1d 2740 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓)) |
14 | 9, 13 | raleqbidv 3336 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓)) |
15 | 7 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥𝐻𝑦) = (𝑋𝐻𝑦)) |
16 | 7, 7 | opeq12d 4812 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 〈𝑥, 𝑥〉 = 〈𝑋, 𝑋〉) |
17 | 16 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (〈𝑥, 𝑥〉 · 𝑦) = (〈𝑋, 𝑋〉 · 𝑦)) |
18 | 17 | oveqd 7292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔)) |
19 | 18 | eqeq1d 2740 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) |
20 | 15, 19 | raleqbidv 3336 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) |
21 | 14, 20 | anbi12d 631 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) |
22 | 21 | ralbidv 3112 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) |
23 | 8, 22 | riotaeqbidv 7235 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) |
24 | | cidval.x |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
25 | | riotaex 7236 |
. . 3
⊢
(℩𝑔
∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) ∈ V |
26 | 25 | a1i 11 |
. 2
⊢ (𝜑 → (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) ∈ V) |
27 | 6, 23, 24, 26 | fvmptd 6882 |
1
⊢ (𝜑 → ( 1 ‘𝑋) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) |