Step | Hyp | Ref
| Expression |
1 | | cbigo 47311 |
. 2
class
ฮ |
2 | | vg |
. . 3
setvar ๐ |
3 | | cr 11111 |
. . . 4
class
โ |
4 | | cpm 8823 |
. . . 4
class
โpm |
5 | 3, 3, 4 | co 7411 |
. . 3
class (โ
โpm โ) |
6 | | vy |
. . . . . . . . . 10
setvar ๐ฆ |
7 | 6 | cv 1540 |
. . . . . . . . 9
class ๐ฆ |
8 | | vf |
. . . . . . . . . 10
setvar ๐ |
9 | 8 | cv 1540 |
. . . . . . . . 9
class ๐ |
10 | 7, 9 | cfv 6543 |
. . . . . . . 8
class (๐โ๐ฆ) |
11 | | vm |
. . . . . . . . . 10
setvar ๐ |
12 | 11 | cv 1540 |
. . . . . . . . 9
class ๐ |
13 | 2 | cv 1540 |
. . . . . . . . . 10
class ๐ |
14 | 7, 13 | cfv 6543 |
. . . . . . . . 9
class (๐โ๐ฆ) |
15 | | cmul 11117 |
. . . . . . . . 9
class
ยท |
16 | 12, 14, 15 | co 7411 |
. . . . . . . 8
class (๐ ยท (๐โ๐ฆ)) |
17 | | cle 11251 |
. . . . . . . 8
class
โค |
18 | 10, 16, 17 | wbr 5148 |
. . . . . . 7
wff (๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
19 | 9 | cdm 5676 |
. . . . . . . 8
class dom ๐ |
20 | | vx |
. . . . . . . . . 10
setvar ๐ฅ |
21 | 20 | cv 1540 |
. . . . . . . . 9
class ๐ฅ |
22 | | cpnf 11247 |
. . . . . . . . 9
class
+โ |
23 | | cico 13328 |
. . . . . . . . 9
class
[,) |
24 | 21, 22, 23 | co 7411 |
. . . . . . . 8
class (๐ฅ[,)+โ) |
25 | 19, 24 | cin 3947 |
. . . . . . 7
class (dom
๐ โฉ (๐ฅ[,)+โ)) |
26 | 18, 6, 25 | wral 3061 |
. . . . . 6
wff
โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
27 | 26, 11, 3 | wrex 3070 |
. . . . 5
wff
โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
28 | 27, 20, 3 | wrex 3070 |
. . . 4
wff
โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) |
29 | 28, 8, 5 | crab 3432 |
. . 3
class {๐ โ (โ
โpm โ) โฃ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} |
30 | 2, 5, 29 | cmpt 5231 |
. 2
class (๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |
31 | 1, 30 | wceq 1541 |
1
wff ฮ =
(๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |