Detailed syntax breakdown of Definition df-inito
Step | Hyp | Ref
| Expression |
1 | | cinito 17346 |
. 2
class
InitO |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | ccat 17031 |
. . 3
class
Cat |
4 | | vh |
. . . . . . . 8
setvar ℎ |
5 | 4 | cv 1541 |
. . . . . . 7
class ℎ |
6 | | va |
. . . . . . . . 9
setvar 𝑎 |
7 | 6 | cv 1541 |
. . . . . . . 8
class 𝑎 |
8 | | vb |
. . . . . . . . 9
setvar 𝑏 |
9 | 8 | cv 1541 |
. . . . . . . 8
class 𝑏 |
10 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑐 |
11 | | chom 16672 |
. . . . . . . . 9
class
Hom |
12 | 10, 11 | cfv 6333 |
. . . . . . . 8
class (Hom
‘𝑐) |
13 | 7, 9, 12 | co 7164 |
. . . . . . 7
class (𝑎(Hom ‘𝑐)𝑏) |
14 | 5, 13 | wcel 2113 |
. . . . . 6
wff ℎ ∈ (𝑎(Hom ‘𝑐)𝑏) |
15 | 14, 4 | weu 2569 |
. . . . 5
wff
∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏) |
16 | | cbs 16579 |
. . . . . 6
class
Base |
17 | 10, 16 | cfv 6333 |
. . . . 5
class
(Base‘𝑐) |
18 | 15, 8, 17 | wral 3053 |
. . . 4
wff
∀𝑏 ∈
(Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏) |
19 | 18, 6, 17 | crab 3057 |
. . 3
class {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)} |
20 | 2, 3, 19 | cmpt 5107 |
. 2
class (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}) |
21 | 1, 20 | wceq 1542 |
1
wff InitO =
(𝑐 ∈ Cat ↦
{𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}) |