| Step |
Hyp |
Ref |
Expression |
| 1 |
|
idfuval.i |
⊢ 𝐼 = ( idfunc ‘ 𝐶 ) |
| 2 |
|
idfuval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
| 3 |
|
idfuval.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
| 4 |
|
idfuval.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
| 5 |
|
fvexd |
⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V ) |
| 6 |
|
fveq2 |
⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) ) |
| 7 |
6 2
|
eqtr4di |
⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 ) |
| 8 |
|
simpr |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 ) |
| 9 |
8
|
reseq2d |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( I ↾ 𝑏 ) = ( I ↾ 𝐵 ) ) |
| 10 |
8
|
sqxpeqd |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) ) |
| 11 |
|
simpl |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 ) |
| 12 |
11
|
fveq2d |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) ) |
| 13 |
12 4
|
eqtr4di |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 ) |
| 14 |
13
|
fveq1d |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) ) |
| 15 |
14
|
reseq2d |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) = ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) |
| 16 |
10 15
|
mpteq12dv |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) |
| 17 |
9 16
|
opeq12d |
⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) |
| 18 |
5 7 17
|
csbied2 |
⊢ ( 𝑐 = 𝐶 → ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) |
| 19 |
|
df-idfu |
⊢ idfunc = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ ) |
| 20 |
|
opex |
⊢ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ∈ V |
| 21 |
18 19 20
|
fvmpt |
⊢ ( 𝐶 ∈ Cat → ( idfunc ‘ 𝐶 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) |
| 22 |
3 21
|
syl |
⊢ ( 𝜑 → ( idfunc ‘ 𝐶 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) |
| 23 |
1 22
|
syl5eq |
⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) |