Step | Hyp | Ref
| Expression |
1 | | cordt 17444 |
. 2
class
ordTop |
2 | | vr |
. . 3
setvar π |
3 | | cvv 3474 |
. . 3
class
V |
4 | 2 | cv 1540 |
. . . . . . . 8
class π |
5 | 4 | cdm 5676 |
. . . . . . 7
class dom π |
6 | 5 | csn 4628 |
. . . . . 6
class {dom
π} |
7 | | vx |
. . . . . . . . 9
setvar π₯ |
8 | | vy |
. . . . . . . . . . . . 13
setvar π¦ |
9 | 8 | cv 1540 |
. . . . . . . . . . . 12
class π¦ |
10 | 7 | cv 1540 |
. . . . . . . . . . . 12
class π₯ |
11 | 9, 10, 4 | wbr 5148 |
. . . . . . . . . . 11
wff π¦ππ₯ |
12 | 11 | wn 3 |
. . . . . . . . . 10
wff Β¬
π¦ππ₯ |
13 | 12, 8, 5 | crab 3432 |
. . . . . . . . 9
class {π¦ β dom π β£ Β¬ π¦ππ₯} |
14 | 7, 5, 13 | cmpt 5231 |
. . . . . . . 8
class (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) |
15 | 10, 9, 4 | wbr 5148 |
. . . . . . . . . . 11
wff π₯ππ¦ |
16 | 15 | wn 3 |
. . . . . . . . . 10
wff Β¬
π₯ππ¦ |
17 | 16, 8, 5 | crab 3432 |
. . . . . . . . 9
class {π¦ β dom π β£ Β¬ π₯ππ¦} |
18 | 7, 5, 17 | cmpt 5231 |
. . . . . . . 8
class (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦}) |
19 | 14, 18 | cun 3946 |
. . . . . . 7
class ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})) |
20 | 19 | crn 5677 |
. . . . . 6
class ran
((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})) |
21 | 6, 20 | cun 3946 |
. . . . 5
class ({dom
π} βͺ ran ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦}))) |
22 | | cfi 9404 |
. . . . 5
class
fi |
23 | 21, 22 | cfv 6543 |
. . . 4
class
(fiβ({dom π}
βͺ ran ((π₯ β dom
π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})))) |
24 | | ctg 17382 |
. . . 4
class
topGen |
25 | 23, 24 | cfv 6543 |
. . 3
class
(topGenβ(fiβ({dom π} βͺ ran ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦}))))) |
26 | 2, 3, 25 | cmpt 5231 |
. 2
class (π β V β¦
(topGenβ(fiβ({dom π} βͺ ran ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})))))) |
27 | 1, 26 | wceq 1541 |
1
wff ordTop =
(π β V β¦
(topGenβ(fiβ({dom π} βͺ ran ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})))))) |