Step | Hyp | Ref
| Expression |
1 | | rankwflemb 9790 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β βπ₯ β On π΄ β (π
1βsuc
π₯)) |
2 | | nfcv 2903 |
. . . . . 6
β’
β²π₯π
1 |
3 | | nfrab1 3451 |
. . . . . . . 8
β’
β²π₯{π₯ β On β£ π΄ β (π
1βsuc
π₯)} |
4 | 3 | nfint 4960 |
. . . . . . 7
β’
β²π₯β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)} |
5 | 4 | nfsuc 6436 |
. . . . . 6
β’
β²π₯ suc
β© {π₯ β On β£ π΄ β (π
1βsuc
π₯)} |
6 | 2, 5 | nffv 6901 |
. . . . 5
β’
β²π₯(π
1βsuc β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)}) |
7 | 6 | nfel2 2921 |
. . . 4
β’
β²π₯ π΄ β
(π
1βsuc β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)}) |
8 | | suceq 6430 |
. . . . . 6
β’ (π₯ = β©
{π₯ β On β£ π΄ β
(π
1βsuc π₯)} β suc π₯ = suc β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)}) |
9 | 8 | fveq2d 6895 |
. . . . 5
β’ (π₯ = β©
{π₯ β On β£ π΄ β
(π
1βsuc π₯)} β (π
1βsuc
π₯) =
(π
1βsuc β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)})) |
10 | 9 | eleq2d 2819 |
. . . 4
β’ (π₯ = β©
{π₯ β On β£ π΄ β
(π
1βsuc π₯)} β (π΄ β (π
1βsuc
π₯) β π΄ β (π
1βsuc
β© {π₯ β On β£ π΄ β (π
1βsuc
π₯)}))) |
11 | 7, 10 | onminsb 7784 |
. . 3
β’
(βπ₯ β On
π΄ β
(π
1βsuc π₯) β π΄ β (π
1βsuc
β© {π₯ β On β£ π΄ β (π
1βsuc
π₯)})) |
12 | 1, 11 | sylbi 216 |
. 2
β’ (π΄ β βͺ (π
1 β On) β π΄ β
(π
1βsuc β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)})) |
13 | | rankvalb 9794 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ΄) = β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)}) |
14 | | suceq 6430 |
. . . 4
β’
((rankβπ΄) =
β© {π₯ β On β£ π΄ β (π
1βsuc
π₯)} β suc
(rankβπ΄) = suc β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)}) |
15 | 13, 14 | syl 17 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β suc
(rankβπ΄) = suc β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)}) |
16 | 15 | fveq2d 6895 |
. 2
β’ (π΄ β βͺ (π
1 β On) β
(π
1βsuc (rankβπ΄)) = (π
1βsuc β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)})) |
17 | 12, 16 | eleqtrrd 2836 |
1
β’ (π΄ β βͺ (π
1 β On) β π΄ β
(π
1βsuc (rankβπ΄))) |