Detailed syntax breakdown of Definition df-idfu
Step | Hyp | Ref
| Expression |
1 | | cidfu 17568 |
. 2
class
idfunc |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | ccat 17371 |
. . 3
class
Cat |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1538 |
. . . . 5
class 𝑡 |
6 | | cbs 16910 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6435 |
. . . 4
class
(Base‘𝑡) |
8 | | cid 5490 |
. . . . . 6
class
I |
9 | 4 | cv 1538 |
. . . . . 6
class 𝑏 |
10 | 8, 9 | cres 5593 |
. . . . 5
class ( I
↾ 𝑏) |
11 | | vz |
. . . . . 6
setvar 𝑧 |
12 | 9, 9 | cxp 5589 |
. . . . . 6
class (𝑏 × 𝑏) |
13 | 11 | cv 1538 |
. . . . . . . 8
class 𝑧 |
14 | | chom 16971 |
. . . . . . . . 9
class
Hom |
15 | 5, 14 | cfv 6435 |
. . . . . . . 8
class (Hom
‘𝑡) |
16 | 13, 15 | cfv 6435 |
. . . . . . 7
class ((Hom
‘𝑡)‘𝑧) |
17 | 8, 16 | cres 5593 |
. . . . . 6
class ( I
↾ ((Hom ‘𝑡)‘𝑧)) |
18 | 11, 12, 17 | cmpt 5159 |
. . . . 5
class (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧))) |
19 | 10, 18 | cop 4569 |
. . . 4
class 〈( I
↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉 |
20 | 4, 7, 19 | csb 3833 |
. . 3
class
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉 |
21 | 2, 3, 20 | cmpt 5159 |
. 2
class (𝑡 ∈ Cat ↦
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) |
22 | 1, 21 | wceq 1539 |
1
wff
idfunc = (𝑡 ∈ Cat ↦
⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) |