Step | Hyp | Ref
| Expression |
1 | | comnd 32210 |
. 2
class
oMnd |
2 | | vg |
. . . . . . . . 9
setvar π |
3 | 2 | cv 1540 |
. . . . . . . 8
class π |
4 | | ctos 18368 |
. . . . . . . 8
class
Toset |
5 | 3, 4 | wcel 2106 |
. . . . . . 7
wff π β Toset |
6 | | va |
. . . . . . . . . . . . 13
setvar π |
7 | 6 | cv 1540 |
. . . . . . . . . . . 12
class π |
8 | | vb |
. . . . . . . . . . . . 13
setvar π |
9 | 8 | cv 1540 |
. . . . . . . . . . . 12
class π |
10 | | vl |
. . . . . . . . . . . . 13
setvar π |
11 | 10 | cv 1540 |
. . . . . . . . . . . 12
class π |
12 | 7, 9, 11 | wbr 5148 |
. . . . . . . . . . 11
wff πππ |
13 | | vc |
. . . . . . . . . . . . . 14
setvar π |
14 | 13 | cv 1540 |
. . . . . . . . . . . . 13
class π |
15 | | vp |
. . . . . . . . . . . . . 14
setvar π |
16 | 15 | cv 1540 |
. . . . . . . . . . . . 13
class π |
17 | 7, 14, 16 | co 7408 |
. . . . . . . . . . . 12
class (πππ) |
18 | 9, 14, 16 | co 7408 |
. . . . . . . . . . . 12
class (πππ) |
19 | 17, 18, 11 | wbr 5148 |
. . . . . . . . . . 11
wff (πππ)π(πππ) |
20 | 12, 19 | wi 4 |
. . . . . . . . . 10
wff (πππ β (πππ)π(πππ)) |
21 | | vv |
. . . . . . . . . . 11
setvar π£ |
22 | 21 | cv 1540 |
. . . . . . . . . 10
class π£ |
23 | 20, 13, 22 | wral 3061 |
. . . . . . . . 9
wff
βπ β
π£ (πππ β (πππ)π(πππ)) |
24 | 23, 8, 22 | wral 3061 |
. . . . . . . 8
wff
βπ β
π£ βπ β π£ (πππ β (πππ)π(πππ)) |
25 | 24, 6, 22 | wral 3061 |
. . . . . . 7
wff
βπ β
π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)) |
26 | 5, 25 | wa 396 |
. . . . . 6
wff (π β Toset β§
βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) |
27 | | cple 17203 |
. . . . . . 7
class
le |
28 | 3, 27 | cfv 6543 |
. . . . . 6
class
(leβπ) |
29 | 26, 10, 28 | wsbc 3777 |
. . . . 5
wff
[(leβπ)
/ π](π β Toset β§
βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) |
30 | | cplusg 17196 |
. . . . . 6
class
+g |
31 | 3, 30 | cfv 6543 |
. . . . 5
class
(+gβπ) |
32 | 29, 15, 31 | wsbc 3777 |
. . . 4
wff
[(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) |
33 | | cbs 17143 |
. . . . 5
class
Base |
34 | 3, 33 | cfv 6543 |
. . . 4
class
(Baseβπ) |
35 | 32, 21, 34 | wsbc 3777 |
. . 3
wff
[(Baseβπ) / π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) |
36 | | cmnd 18624 |
. . 3
class
Mnd |
37 | 35, 2, 36 | crab 3432 |
. 2
class {π β Mnd β£
[(Baseβπ) /
π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)))} |
38 | 1, 37 | wceq 1541 |
1
wff oMnd =
{π β Mnd β£
[(Baseβπ) /
π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)))} |