Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class π΄ |
2 | 1 | wsmo 8292 |
. 2
wff Smo π΄ |
3 | 1 | cdm 5634 |
. . . 4
class dom π΄ |
4 | | con0 6318 |
. . . 4
class
On |
5 | 3, 4, 1 | wf 6493 |
. . 3
wff π΄:dom π΄βΆOn |
6 | 3 | word 6317 |
. . 3
wff Ord dom
π΄ |
7 | | vx |
. . . . . . 7
setvar π₯ |
8 | | vy |
. . . . . . 7
setvar π¦ |
9 | 7, 8 | wel 2108 |
. . . . . 6
wff π₯ β π¦ |
10 | 7 | cv 1541 |
. . . . . . . 8
class π₯ |
11 | 10, 1 | cfv 6497 |
. . . . . . 7
class (π΄βπ₯) |
12 | 8 | cv 1541 |
. . . . . . . 8
class π¦ |
13 | 12, 1 | cfv 6497 |
. . . . . . 7
class (π΄βπ¦) |
14 | 11, 13 | wcel 2107 |
. . . . . 6
wff (π΄βπ₯) β (π΄βπ¦) |
15 | 9, 14 | wi 4 |
. . . . 5
wff (π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) |
16 | 15, 8, 3 | wral 3061 |
. . . 4
wff
βπ¦ β dom
π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) |
17 | 16, 7, 3 | wral 3061 |
. . 3
wff
βπ₯ β dom
π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) |
18 | 5, 6, 17 | w3a 1088 |
. 2
wff (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
19 | 2, 18 | wb 205 |
1
wff (Smo π΄ β (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |