Step | Hyp | Ref
| Expression |
1 | | cdrs 18247 |
. 2
class
Dirset |
2 | | vb |
. . . . . . . 8
setvar π |
3 | 2 | cv 1541 |
. . . . . . 7
class π |
4 | | c0 4323 |
. . . . . . 7
class
β
|
5 | 3, 4 | wne 2941 |
. . . . . 6
wff π β β
|
6 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
7 | 6 | cv 1541 |
. . . . . . . . . . 11
class π₯ |
8 | | vz |
. . . . . . . . . . . 12
setvar π§ |
9 | 8 | cv 1541 |
. . . . . . . . . . 11
class π§ |
10 | | vr |
. . . . . . . . . . . 12
setvar π |
11 | 10 | cv 1541 |
. . . . . . . . . . 11
class π |
12 | 7, 9, 11 | wbr 5149 |
. . . . . . . . . 10
wff π₯ππ§ |
13 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
14 | 13 | cv 1541 |
. . . . . . . . . . 11
class π¦ |
15 | 14, 9, 11 | wbr 5149 |
. . . . . . . . . 10
wff π¦ππ§ |
16 | 12, 15 | wa 397 |
. . . . . . . . 9
wff (π₯ππ§ β§ π¦ππ§) |
17 | 16, 8, 3 | wrex 3071 |
. . . . . . . 8
wff
βπ§ β
π (π₯ππ§ β§ π¦ππ§) |
18 | 17, 13, 3 | wral 3062 |
. . . . . . 7
wff
βπ¦ β
π βπ§ β π (π₯ππ§ β§ π¦ππ§) |
19 | 18, 6, 3 | wral 3062 |
. . . . . 6
wff
βπ₯ β
π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§) |
20 | 5, 19 | wa 397 |
. . . . 5
wff (π β β
β§
βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) |
21 | | vf |
. . . . . . 7
setvar π |
22 | 21 | cv 1541 |
. . . . . 6
class π |
23 | | cple 17204 |
. . . . . 6
class
le |
24 | 22, 23 | cfv 6544 |
. . . . 5
class
(leβπ) |
25 | 20, 10, 24 | wsbc 3778 |
. . . 4
wff
[(leβπ)
/ π](π β β
β§
βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) |
26 | | cbs 17144 |
. . . . 5
class
Base |
27 | 22, 26 | cfv 6544 |
. . . 4
class
(Baseβπ) |
28 | 25, 2, 27 | wsbc 3778 |
. . 3
wff
[(Baseβπ) / π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) |
29 | | cproset 18246 |
. . 3
class
Proset |
30 | 28, 21, 29 | crab 3433 |
. 2
class {π β Proset β£
[(Baseβπ) /
π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§))} |
31 | 1, 30 | wceq 1542 |
1
wff Dirset =
{π β Proset β£
[(Baseβπ) /
π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§))} |