Detailed syntax breakdown of Definition df-full
Step | Hyp | Ref
| Expression |
1 | | cful 17534 |
. 2
class
Full |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vd |
. . 3
setvar 𝑑 |
4 | | ccat 17290 |
. . 3
class
Cat |
5 | | vf |
. . . . . . 7
setvar 𝑓 |
6 | 5 | cv 1538 |
. . . . . 6
class 𝑓 |
7 | | vg |
. . . . . . 7
setvar 𝑔 |
8 | 7 | cv 1538 |
. . . . . 6
class 𝑔 |
9 | 2 | cv 1538 |
. . . . . . 7
class 𝑐 |
10 | 3 | cv 1538 |
. . . . . . 7
class 𝑑 |
11 | | cfunc 17485 |
. . . . . . 7
class
Func |
12 | 9, 10, 11 | co 7255 |
. . . . . 6
class (𝑐 Func 𝑑) |
13 | 6, 8, 12 | wbr 5070 |
. . . . 5
wff 𝑓(𝑐 Func 𝑑)𝑔 |
14 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
15 | 14 | cv 1538 |
. . . . . . . . . 10
class 𝑥 |
16 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
17 | 16 | cv 1538 |
. . . . . . . . . 10
class 𝑦 |
18 | 15, 17, 8 | co 7255 |
. . . . . . . . 9
class (𝑥𝑔𝑦) |
19 | 18 | crn 5581 |
. . . . . . . 8
class ran
(𝑥𝑔𝑦) |
20 | 15, 6 | cfv 6418 |
. . . . . . . . 9
class (𝑓‘𝑥) |
21 | 17, 6 | cfv 6418 |
. . . . . . . . 9
class (𝑓‘𝑦) |
22 | | chom 16899 |
. . . . . . . . . 10
class
Hom |
23 | 10, 22 | cfv 6418 |
. . . . . . . . 9
class (Hom
‘𝑑) |
24 | 20, 21, 23 | co 7255 |
. . . . . . . 8
class ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)) |
25 | 19, 24 | wceq 1539 |
. . . . . . 7
wff ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)) |
26 | | cbs 16840 |
. . . . . . . 8
class
Base |
27 | 9, 26 | cfv 6418 |
. . . . . . 7
class
(Base‘𝑐) |
28 | 25, 16, 27 | wral 3063 |
. . . . . 6
wff
∀𝑦 ∈
(Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)) |
29 | 28, 14, 27 | wral 3063 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)) |
30 | 13, 29 | wa 395 |
. . . 4
wff (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))) |
31 | 30, 5, 7 | copab 5132 |
. . 3
class
{〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} |
32 | 2, 3, 4, 4, 31 | cmpo 7257 |
. 2
class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) |
33 | 1, 32 | wceq 1539 |
1
wff Full =
(𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) |