Step | Hyp | Ref
| Expression |
1 | | cbigo 47233 |
. 2
class
ฮ |
2 | | vg |
. . 3
setvar ๐ |
3 | | cr 11109 |
. . . 4
class
โ |
4 | | cpm 8821 |
. . . 4
class
โpm |
5 | 3, 3, 4 | co 7409 |
. . 3
class (โ
โpm โ) |
6 | | vy |
. . . . . . . . . 10
setvar ๐ฆ |
7 | 6 | cv 1541 |
. . . . . . . . 9
class ๐ฆ |
8 | | vf |
. . . . . . . . . 10
setvar ๐ |
9 | 8 | cv 1541 |
. . . . . . . . 9
class ๐ |
10 | 7, 9 | cfv 6544 |
. . . . . . . 8
class (๐โ๐ฆ) |
11 | | vm |
. . . . . . . . . 10
setvar ๐ |
12 | 11 | cv 1541 |
. . . . . . . . 9
class ๐ |
13 | 2 | cv 1541 |
. . . . . . . . . 10
class ๐ |
14 | 7, 13 | cfv 6544 |
. . . . . . . . 9
class (๐โ๐ฆ) |
15 | | cmul 11115 |
. . . . . . . . 9
class
ยท |
16 | 12, 14, 15 | co 7409 |
. . . . . . . 8
class (๐ ยท (๐โ๐ฆ)) |
17 | | cle 11249 |
. . . . . . . 8
class
โค |
18 | 10, 16, 17 | wbr 5149 |
. . . . . . 7
wff (๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
19 | 9 | cdm 5677 |
. . . . . . . 8
class dom ๐ |
20 | | vx |
. . . . . . . . . 10
setvar ๐ฅ |
21 | 20 | cv 1541 |
. . . . . . . . 9
class ๐ฅ |
22 | | cpnf 11245 |
. . . . . . . . 9
class
+โ |
23 | | cico 13326 |
. . . . . . . . 9
class
[,) |
24 | 21, 22, 23 | co 7409 |
. . . . . . . 8
class (๐ฅ[,)+โ) |
25 | 19, 24 | cin 3948 |
. . . . . . 7
class (dom
๐ โฉ (๐ฅ[,)+โ)) |
26 | 18, 6, 25 | wral 3062 |
. . . . . 6
wff
โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
27 | 26, 11, 3 | wrex 3071 |
. . . . 5
wff
โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
28 | 27, 20, 3 | wrex 3071 |
. . . 4
wff
โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
29 | 28, 8, 5 | crab 3433 |
. . 3
class {๐ โ (โ
โpm โ) โฃ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} |
30 | 2, 5, 29 | cmpt 5232 |
. 2
class (๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |
31 | 1, 30 | wceq 1542 |
1
wff ฮ =
(๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |