Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class π΄ |
2 | 1 | cnlly 23289 |
. 2
class
π-Locally π΄ |
3 | | vj |
. . . . . . . . 9
setvar π |
4 | 3 | cv 1539 |
. . . . . . . 8
class π |
5 | | vu |
. . . . . . . . 9
setvar π’ |
6 | 5 | cv 1539 |
. . . . . . . 8
class π’ |
7 | | crest 17373 |
. . . . . . . 8
class
βΎt |
8 | 4, 6, 7 | co 7412 |
. . . . . . 7
class (π βΎt π’) |
9 | 8, 1 | wcel 2105 |
. . . . . 6
wff (π βΎt π’) β π΄ |
10 | | vy |
. . . . . . . . . 10
setvar π¦ |
11 | 10 | cv 1539 |
. . . . . . . . 9
class π¦ |
12 | 11 | csn 4628 |
. . . . . . . 8
class {π¦} |
13 | | cnei 22921 |
. . . . . . . . 9
class
nei |
14 | 4, 13 | cfv 6543 |
. . . . . . . 8
class
(neiβπ) |
15 | 12, 14 | cfv 6543 |
. . . . . . 7
class
((neiβπ)β{π¦}) |
16 | | vx |
. . . . . . . . 9
setvar π₯ |
17 | 16 | cv 1539 |
. . . . . . . 8
class π₯ |
18 | 17 | cpw 4602 |
. . . . . . 7
class π«
π₯ |
19 | 15, 18 | cin 3947 |
. . . . . 6
class
(((neiβπ)β{π¦}) β© π« π₯) |
20 | 9, 5, 19 | wrex 3069 |
. . . . 5
wff
βπ’ β
(((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ |
21 | 20, 10, 17 | wral 3060 |
. . . 4
wff
βπ¦ β
π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ |
22 | 21, 16, 4 | wral 3060 |
. . 3
wff
βπ₯ β
π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ |
23 | | ctop 22715 |
. . 3
class
Top |
24 | 22, 3, 23 | crab 3431 |
. 2
class {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} |
25 | 2, 24 | wceq 1540 |
1
wff
π-Locally π΄
= {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} |