Step | Hyp | Ref
| Expression |
1 | | csubc 17699 |
. 2
class
Subcat |
2 | | vc |
. . 3
setvar π |
3 | | ccat 17551 |
. . 3
class
Cat |
4 | | vh |
. . . . . . 7
setvar β |
5 | 4 | cv 1541 |
. . . . . 6
class β |
6 | 2 | cv 1541 |
. . . . . . 7
class π |
7 | | chomf 17553 |
. . . . . . 7
class
Homf |
8 | 6, 7 | cfv 6501 |
. . . . . 6
class
(Homf βπ) |
9 | | cssc 17697 |
. . . . . 6
class
βcat |
10 | 5, 8, 9 | wbr 5110 |
. . . . 5
wff β βcat
(Homf βπ) |
11 | | vx |
. . . . . . . . . . 11
setvar π₯ |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class π₯ |
13 | | ccid 17552 |
. . . . . . . . . . 11
class
Id |
14 | 6, 13 | cfv 6501 |
. . . . . . . . . 10
class
(Idβπ) |
15 | 12, 14 | cfv 6501 |
. . . . . . . . 9
class
((Idβπ)βπ₯) |
16 | 12, 12, 5 | co 7362 |
. . . . . . . . 9
class (π₯βπ₯) |
17 | 15, 16 | wcel 2107 |
. . . . . . . 8
wff
((Idβπ)βπ₯) β (π₯βπ₯) |
18 | | vg |
. . . . . . . . . . . . . . 15
setvar π |
19 | 18 | cv 1541 |
. . . . . . . . . . . . . 14
class π |
20 | | vf |
. . . . . . . . . . . . . . 15
setvar π |
21 | 20 | cv 1541 |
. . . . . . . . . . . . . 14
class π |
22 | | vy |
. . . . . . . . . . . . . . . . 17
setvar π¦ |
23 | 22 | cv 1541 |
. . . . . . . . . . . . . . . 16
class π¦ |
24 | 12, 23 | cop 4597 |
. . . . . . . . . . . . . . 15
class
β¨π₯, π¦β© |
25 | | vz |
. . . . . . . . . . . . . . . 16
setvar π§ |
26 | 25 | cv 1541 |
. . . . . . . . . . . . . . 15
class π§ |
27 | | cco 17152 |
. . . . . . . . . . . . . . . 16
class
comp |
28 | 6, 27 | cfv 6501 |
. . . . . . . . . . . . . . 15
class
(compβπ) |
29 | 24, 26, 28 | co 7362 |
. . . . . . . . . . . . . 14
class
(β¨π₯, π¦β©(compβπ)π§) |
30 | 19, 21, 29 | co 7362 |
. . . . . . . . . . . . 13
class (π(β¨π₯, π¦β©(compβπ)π§)π) |
31 | 12, 26, 5 | co 7362 |
. . . . . . . . . . . . 13
class (π₯βπ§) |
32 | 30, 31 | wcel 2107 |
. . . . . . . . . . . 12
wff (π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§) |
33 | 23, 26, 5 | co 7362 |
. . . . . . . . . . . 12
class (π¦βπ§) |
34 | 32, 18, 33 | wral 3065 |
. . . . . . . . . . 11
wff
βπ β
(π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§) |
35 | 12, 23, 5 | co 7362 |
. . . . . . . . . . 11
class (π₯βπ¦) |
36 | 34, 20, 35 | wral 3065 |
. . . . . . . . . 10
wff
βπ β
(π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§) |
37 | | vs |
. . . . . . . . . . 11
setvar π |
38 | 37 | cv 1541 |
. . . . . . . . . 10
class π |
39 | 36, 25, 38 | wral 3065 |
. . . . . . . . 9
wff
βπ§ β
π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§) |
40 | 39, 22, 38 | wral 3065 |
. . . . . . . 8
wff
βπ¦ β
π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§) |
41 | 17, 40 | wa 397 |
. . . . . . 7
wff
(((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)) |
42 | 41, 11, 38 | wral 3065 |
. . . . . 6
wff
βπ₯ β
π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)) |
43 | 5 | cdm 5638 |
. . . . . . 7
class dom β |
44 | 43 | cdm 5638 |
. . . . . 6
class dom dom
β |
45 | 42, 37, 44 | wsbc 3744 |
. . . . 5
wff [dom
dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)) |
46 | 10, 45 | wa 397 |
. . . 4
wff (β βcat
(Homf βπ) β§ [dom dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§))) |
47 | 46, 4 | cab 2714 |
. . 3
class {β β£ (β βcat (Homf
βπ) β§ [dom
dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)))} |
48 | 2, 3, 47 | cmpt 5193 |
. 2
class (π β Cat β¦ {β β£ (β βcat (Homf
βπ) β§ [dom
dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)))}) |
49 | 1, 48 | wceq 1542 |
1
wff Subcat =
(π β Cat β¦
{β β£ (β βcat
(Homf βπ) β§ [dom dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)))}) |