Detailed syntax breakdown of Definition df-idfu
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cidfu 17900 | . 2
class
idfunc | 
| 2 |  | vt | . . 3
setvar 𝑡 | 
| 3 |  | ccat 17707 | . . 3
class
Cat | 
| 4 |  | vb | . . . 4
setvar 𝑏 | 
| 5 | 2 | cv 1539 | . . . . 5
class 𝑡 | 
| 6 |  | cbs 17247 | . . . . 5
class
Base | 
| 7 | 5, 6 | cfv 6561 | . . . 4
class
(Base‘𝑡) | 
| 8 |  | cid 5577 | . . . . . 6
class 
I | 
| 9 | 4 | cv 1539 | . . . . . 6
class 𝑏 | 
| 10 | 8, 9 | cres 5687 | . . . . 5
class ( I
↾ 𝑏) | 
| 11 |  | vz | . . . . . 6
setvar 𝑧 | 
| 12 | 9, 9 | cxp 5683 | . . . . . 6
class (𝑏 × 𝑏) | 
| 13 | 11 | cv 1539 | . . . . . . . 8
class 𝑧 | 
| 14 |  | chom 17308 | . . . . . . . . 9
class
Hom | 
| 15 | 5, 14 | cfv 6561 | . . . . . . . 8
class (Hom
‘𝑡) | 
| 16 | 13, 15 | cfv 6561 | . . . . . . 7
class ((Hom
‘𝑡)‘𝑧) | 
| 17 | 8, 16 | cres 5687 | . . . . . 6
class ( I
↾ ((Hom ‘𝑡)‘𝑧)) | 
| 18 | 11, 12, 17 | cmpt 5225 | . . . . 5
class (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧))) | 
| 19 | 10, 18 | cop 4632 | . . . 4
class 〈( I
↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉 | 
| 20 | 4, 7, 19 | csb 3899 | . . 3
class
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉 | 
| 21 | 2, 3, 20 | cmpt 5225 | . 2
class (𝑡 ∈ Cat ↦
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) | 
| 22 | 1, 21 | wceq 1540 | 1
wff
idfunc = (𝑡 ∈ Cat ↦
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) |