Detailed syntax breakdown of Definition df-ida
Step | Hyp | Ref
| Expression |
1 | | cida 17779 |
. 2
class
Ida |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | ccat 17384 |
. . 3
class
Cat |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑐 |
6 | | cbs 16923 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6432 |
. . . 4
class
(Base‘𝑐) |
8 | 4 | cv 1541 |
. . . . 5
class 𝑥 |
9 | | ccid 17385 |
. . . . . . 7
class
Id |
10 | 5, 9 | cfv 6432 |
. . . . . 6
class
(Id‘𝑐) |
11 | 8, 10 | cfv 6432 |
. . . . 5
class
((Id‘𝑐)‘𝑥) |
12 | 8, 8, 11 | cotp 4575 |
. . . 4
class
〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉 |
13 | 4, 7, 12 | cmpt 5162 |
. . 3
class (𝑥 ∈ (Base‘𝑐) ↦ 〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉) |
14 | 2, 3, 13 | cmpt 5162 |
. 2
class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ 〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉)) |
15 | 1, 14 | wceq 1542 |
1
wff
Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ 〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉)) |