Detailed syntax breakdown of Definition df-termo
Step | Hyp | Ref
| Expression |
1 | | ctermo 17697 |
. 2
class
TermO |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | ccat 17373 |
. . 3
class
Cat |
4 | | vh |
. . . . . . . 8
setvar ℎ |
5 | 4 | cv 1538 |
. . . . . . 7
class ℎ |
6 | | vb |
. . . . . . . . 9
setvar 𝑏 |
7 | 6 | cv 1538 |
. . . . . . . 8
class 𝑏 |
8 | | va |
. . . . . . . . 9
setvar 𝑎 |
9 | 8 | cv 1538 |
. . . . . . . 8
class 𝑎 |
10 | 2 | cv 1538 |
. . . . . . . . 9
class 𝑐 |
11 | | chom 16973 |
. . . . . . . . 9
class
Hom |
12 | 10, 11 | cfv 6433 |
. . . . . . . 8
class (Hom
‘𝑐) |
13 | 7, 9, 12 | co 7275 |
. . . . . . 7
class (𝑏(Hom ‘𝑐)𝑎) |
14 | 5, 13 | wcel 2106 |
. . . . . 6
wff ℎ ∈ (𝑏(Hom ‘𝑐)𝑎) |
15 | 14, 4 | weu 2568 |
. . . . 5
wff
∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎) |
16 | | cbs 16912 |
. . . . . 6
class
Base |
17 | 10, 16 | cfv 6433 |
. . . . 5
class
(Base‘𝑐) |
18 | 15, 6, 17 | wral 3064 |
. . . 4
wff
∀𝑏 ∈
(Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎) |
19 | 18, 8, 17 | crab 3068 |
. . 3
class {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)} |
20 | 2, 3, 19 | cmpt 5157 |
. 2
class (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)}) |
21 | 1, 20 | wceq 1539 |
1
wff TermO =
(𝑐 ∈ Cat ↦
{𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)}) |