Step | Hyp | Ref
| Expression |
1 | | df-rank 9760 |
. . . 4
β’ rank =
(π₯ β V β¦ β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)}) |
2 | 1 | funmpt2 6588 |
. . 3
β’ Fun
rank |
3 | | mptv 5265 |
. . . . . 6
β’ (π₯ β V β¦ β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)}) = {β¨π₯, π§β© β£ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)}} |
4 | 1, 3 | eqtri 2761 |
. . . . 5
β’ rank =
{β¨π₯, π§β© β£ π§ = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}} |
5 | 4 | dmeqi 5905 |
. . . 4
β’ dom rank
= dom {β¨π₯, π§β© β£ π§ = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}} |
6 | | dmopab 5916 |
. . . . 5
β’ dom
{β¨π₯, π§β© β£ π§ = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}} = {π₯ β£ βπ§ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)}} |
7 | | eqabcb 2876 |
. . . . . 6
β’ ({π₯ β£ βπ§ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)}} = βͺ
(π
1 β On) β βπ₯(βπ§ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)} β π₯ β βͺ
(π
1 β On))) |
8 | | rankwflemb 9788 |
. . . . . . 7
β’ (π₯ β βͺ (π
1 β On) β βπ¦ β On π₯ β (π
1βsuc
π¦)) |
9 | | intexrab 5341 |
. . . . . . 7
β’
(βπ¦ β On
π₯ β
(π
1βsuc π¦) β β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)} β V) |
10 | | isset 3488 |
. . . . . . 7
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β V β βπ§ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)}) |
11 | 8, 9, 10 | 3bitrri 298 |
. . . . . 6
β’
(βπ§ π§ = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)} β π₯ β βͺ
(π
1 β On)) |
12 | 7, 11 | mpgbir 1802 |
. . . . 5
β’ {π₯ β£ βπ§ π§ = β© {π¦ β On β£ π₯ β
(π
1βsuc π¦)}} = βͺ
(π
1 β On) |
13 | 6, 12 | eqtri 2761 |
. . . 4
β’ dom
{β¨π₯, π§β© β£ π§ = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}} = βͺ
(π
1 β On) |
14 | 5, 13 | eqtri 2761 |
. . 3
β’ dom rank
= βͺ (π
1 β
On) |
15 | | df-fn 6547 |
. . 3
β’ (rank Fn
βͺ (π
1 β On) β (Fun
rank β§ dom rank = βͺ (π
1
β On))) |
16 | 2, 14, 15 | mpbir2an 710 |
. 2
β’ rank Fn
βͺ (π
1 β
On) |
17 | | rabn0 4386 |
. . . . 5
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
β βπ¦ β On π₯ β (π
1βsuc
π¦)) |
18 | 8, 17 | bitr4i 278 |
. . . 4
β’ (π₯ β βͺ (π
1 β On) β {π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
) |
19 | | intex 5338 |
. . . . . 6
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
β β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β V) |
20 | | vex 3479 |
. . . . . . 7
β’ π₯ β V |
21 | 1 | fvmpt2 7010 |
. . . . . . 7
β’ ((π₯ β V β§ β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β V) β (rankβπ₯) = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}) |
22 | 20, 21 | mpan 689 |
. . . . . 6
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β V β (rankβπ₯) = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}) |
23 | 19, 22 | sylbi 216 |
. . . . 5
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
β (rankβπ₯) = β©
{π¦ β On β£ π₯ β
(π
1βsuc π¦)}) |
24 | | ssrab2 4078 |
. . . . . 6
β’ {π¦ β On β£ π₯ β
(π
1βsuc π¦)} β On |
25 | | oninton 7783 |
. . . . . 6
β’ (({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β On β§ {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β β
) β
β© {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β
On) |
26 | 24, 25 | mpan 689 |
. . . . 5
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
β β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β On) |
27 | 23, 26 | eqeltrd 2834 |
. . . 4
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β β
β (rankβπ₯) β On) |
28 | 18, 27 | sylbi 216 |
. . 3
β’ (π₯ β βͺ (π
1 β On) β
(rankβπ₯) β
On) |
29 | 28 | rgen 3064 |
. 2
β’
βπ₯ β
βͺ (π
1 β
On)(rankβπ₯) β
On |
30 | | ffnfv 7118 |
. 2
β’
(rank:βͺ (π
1 β
On)βΆOn β (rank Fn βͺ
(π
1 β On) β§ βπ₯ β βͺ
(π
1 β On)(rankβπ₯) β On)) |
31 | 16, 29, 30 | mpbir2an 710 |
1
β’
rank:βͺ (π
1 β
On)βΆOn |