Detailed syntax breakdown of Definition df-coa
Step | Hyp | Ref
| Expression |
1 | | ccoa 17560 |
. 2
class
compa |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | ccat 17167 |
. . 3
class
Cat |
4 | | vg |
. . . 4
setvar 𝑔 |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑐 |
7 | | carw 17528 |
. . . . 5
class
Arrow |
8 | 6, 7 | cfv 6380 |
. . . 4
class
(Arrow‘𝑐) |
9 | | vh |
. . . . . . . 8
setvar ℎ |
10 | 9 | cv 1542 |
. . . . . . 7
class ℎ |
11 | | ccoda 17527 |
. . . . . . 7
class
coda |
12 | 10, 11 | cfv 6380 |
. . . . . 6
class
(coda‘ℎ) |
13 | 4 | cv 1542 |
. . . . . . 7
class 𝑔 |
14 | | cdoma 17526 |
. . . . . . 7
class
doma |
15 | 13, 14 | cfv 6380 |
. . . . . 6
class
(doma‘𝑔) |
16 | 12, 15 | wceq 1543 |
. . . . 5
wff
(coda‘ℎ) = (doma‘𝑔) |
17 | 16, 9, 8 | crab 3065 |
. . . 4
class {ℎ ∈ (Arrow‘𝑐) ∣
(coda‘ℎ) = (doma‘𝑔)} |
18 | 5 | cv 1542 |
. . . . . 6
class 𝑓 |
19 | 18, 14 | cfv 6380 |
. . . . 5
class
(doma‘𝑓) |
20 | 13, 11 | cfv 6380 |
. . . . 5
class
(coda‘𝑔) |
21 | | c2nd 7760 |
. . . . . . 7
class
2nd |
22 | 13, 21 | cfv 6380 |
. . . . . 6
class
(2nd ‘𝑔) |
23 | 18, 21 | cfv 6380 |
. . . . . 6
class
(2nd ‘𝑓) |
24 | 19, 15 | cop 4547 |
. . . . . . 7
class
〈(doma‘𝑓), (doma‘𝑔)〉 |
25 | | cco 16814 |
. . . . . . . 8
class
comp |
26 | 6, 25 | cfv 6380 |
. . . . . . 7
class
(comp‘𝑐) |
27 | 24, 20, 26 | co 7213 |
. . . . . 6
class
(〈(doma‘𝑓), (doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔)) |
28 | 22, 23, 27 | co 7213 |
. . . . 5
class
((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓)) |
29 | 19, 20, 28 | cotp 4549 |
. . . 4
class
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉 |
30 | 4, 5, 8, 17, 29 | cmpo 7215 |
. . 3
class (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) =
(doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉) |
31 | 2, 3, 30 | cmpt 5135 |
. 2
class (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) =
(doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉)) |
32 | 1, 31 | wceq 1543 |
1
wff
compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) =
(doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉)) |