Step | Hyp | Ref
| Expression |
1 | | 1n0 8434 |
. . . . . . 7
β’
1o β β
|
2 | | neeq1 3006 |
. . . . . . 7
β’
((rankβπ΄) =
1o β ((rankβπ΄) β β
β 1o β
β
)) |
3 | 1, 2 | mpbiri 257 |
. . . . . 6
β’
((rankβπ΄) =
1o β (rankβπ΄) β β
) |
4 | 3 | neneqd 2948 |
. . . . 5
β’
((rankβπ΄) =
1o β Β¬ (rankβπ΄) = β
) |
5 | | fvprc 6834 |
. . . . 5
β’ (Β¬
π΄ β V β
(rankβπ΄) =
β
) |
6 | 4, 5 | nsyl2 141 |
. . . 4
β’
((rankβπ΄) =
1o β π΄
β V) |
7 | | fveqeq2 6851 |
. . . . . 6
β’ (π₯ = π΄ β ((rankβπ₯) = 1o β (rankβπ΄) =
1o)) |
8 | | eqeq1 2740 |
. . . . . 6
β’ (π₯ = π΄ β (π₯ = 1o β π΄ = 1o)) |
9 | 7, 8 | imbi12d 344 |
. . . . 5
β’ (π₯ = π΄ β (((rankβπ₯) = 1o β π₯ = 1o) β ((rankβπ΄) = 1o β π΄ =
1o))) |
10 | | neeq1 3006 |
. . . . . . . 8
β’
((rankβπ₯) =
1o β ((rankβπ₯) β β
β 1o β
β
)) |
11 | 1, 10 | mpbiri 257 |
. . . . . . 7
β’
((rankβπ₯) =
1o β (rankβπ₯) β β
) |
12 | | vex 3449 |
. . . . . . . . 9
β’ π₯ β V |
13 | 12 | rankeq0 9797 |
. . . . . . . 8
β’ (π₯ = β
β
(rankβπ₯) =
β
) |
14 | 13 | necon3bii 2996 |
. . . . . . 7
β’ (π₯ β β
β
(rankβπ₯) β
β
) |
15 | 11, 14 | sylibr 233 |
. . . . . 6
β’
((rankβπ₯) =
1o β π₯ β
β
) |
16 | 12 | rankval 9752 |
. . . . . . . 8
β’
(rankβπ₯) =
β© {π¦ β On β£ π₯ β (π
1βsuc
π¦)} |
17 | 16 | eqeq1i 2741 |
. . . . . . 7
β’
((rankβπ₯) =
1o β β© {π¦ β On β£ π₯ β (π
1βsuc
π¦)} =
1o) |
18 | | ssrab2 4037 |
. . . . . . . . . . 11
β’ {π¦ β On β£ π₯ β
(π
1βsuc π¦)} β On |
19 | | elirr 9533 |
. . . . . . . . . . . . . 14
β’ Β¬
1o β 1o |
20 | | 1oex 8422 |
. . . . . . . . . . . . . . 15
β’
1o β V |
21 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (V =
1o β V = 1o) |
22 | 20, 21 | eleqtrid 2843 |
. . . . . . . . . . . . . 14
β’ (V =
1o β 1o β 1o) |
23 | 19, 22 | mto 196 |
. . . . . . . . . . . . 13
β’ Β¬ V
= 1o |
24 | | inteq 4910 |
. . . . . . . . . . . . . . 15
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} = β
β β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = β©
β
) |
25 | | int0 4923 |
. . . . . . . . . . . . . . 15
β’ β© β
= V |
26 | 24, 25 | eqtrdi 2792 |
. . . . . . . . . . . . . 14
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} = β
β β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = V) |
27 | 26 | eqeq1d 2738 |
. . . . . . . . . . . . 13
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} = β
β (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β V =
1o)) |
28 | 23, 27 | mtbiri 326 |
. . . . . . . . . . . 12
β’ ({π¦ β On β£ π₯ β
(π
1βsuc π¦)} = β
β Β¬ β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o) |
29 | 28 | necon2ai 2973 |
. . . . . . . . . . 11
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β
β
) |
30 | | onint 7725 |
. . . . . . . . . . 11
β’ (({π¦ β On β£ π₯ β
(π
1βsuc π¦)} β On β§ {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β β
) β
β© {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β {π¦ β On β£ π₯ β
(π
1βsuc π¦)}) |
31 | 18, 29, 30 | sylancr 587 |
. . . . . . . . . 10
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β {π¦ β On β£ π₯ β (π
1βsuc
π¦)}) |
32 | | eleq1 2825 |
. . . . . . . . . 10
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} β {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β 1o
β {π¦ β On β£
π₯ β
(π
1βsuc π¦)})) |
33 | 31, 32 | mpbid 231 |
. . . . . . . . 9
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β 1o
β {π¦ β On β£
π₯ β
(π
1βsuc π¦)}) |
34 | | suceq 6383 |
. . . . . . . . . . . . 13
β’ (π¦ = 1o β suc
π¦ = suc
1o) |
35 | 34 | fveq2d 6846 |
. . . . . . . . . . . 12
β’ (π¦ = 1o β
(π
1βsuc π¦) = (π
1βsuc
1o)) |
36 | | df-1o 8412 |
. . . . . . . . . . . . . . . . 17
β’
1o = suc β
|
37 | 36 | fveq2i 6845 |
. . . . . . . . . . . . . . . 16
β’
(π
1β1o) =
(π
1βsuc β
) |
38 | | 0elon 6371 |
. . . . . . . . . . . . . . . . 17
β’ β
β On |
39 | | r1suc 9706 |
. . . . . . . . . . . . . . . . 17
β’ (β
β On β (π
1βsuc β
) = π«
(π
1ββ
)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(π
1βsuc β
) = π«
(π
1ββ
) |
41 | | r10 9704 |
. . . . . . . . . . . . . . . . 17
β’
(π
1ββ
) = β
|
42 | 41 | pweqi 4576 |
. . . . . . . . . . . . . . . 16
β’ π«
(π
1ββ
) = π« β
|
43 | 37, 40, 42 | 3eqtri 2768 |
. . . . . . . . . . . . . . 15
β’
(π
1β1o) = π«
β
|
44 | 43 | pweqi 4576 |
. . . . . . . . . . . . . 14
β’ π«
(π
1β1o) = π« π«
β
|
45 | | pw0 4772 |
. . . . . . . . . . . . . . 15
β’ π«
β
= {β
} |
46 | 45 | pweqi 4576 |
. . . . . . . . . . . . . 14
β’ π«
π« β
= π« {β
} |
47 | | pwpw0 4773 |
. . . . . . . . . . . . . 14
β’ π«
{β
} = {β
, {β
}} |
48 | 44, 46, 47 | 3eqtrri 2769 |
. . . . . . . . . . . . 13
β’ {β
,
{β
}} = π«
(π
1β1o) |
49 | | 1on 8424 |
. . . . . . . . . . . . . 14
β’
1o β On |
50 | | r1suc 9706 |
. . . . . . . . . . . . . 14
β’
(1o β On β (π
1βsuc
1o) = π«
(π
1β1o)) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(π
1βsuc 1o) = π«
(π
1β1o) |
52 | 48, 51 | eqtr4i 2767 |
. . . . . . . . . . . 12
β’ {β
,
{β
}} = (π
1βsuc 1o) |
53 | 35, 52 | eqtr4di 2794 |
. . . . . . . . . . 11
β’ (π¦ = 1o β
(π
1βsuc π¦) = {β
, {β
}}) |
54 | 53 | eleq2d 2823 |
. . . . . . . . . 10
β’ (π¦ = 1o β (π₯ β
(π
1βsuc π¦) β π₯ β {β
,
{β
}})) |
55 | 54 | elrab 3645 |
. . . . . . . . 9
β’
(1o β {π¦ β On β£ π₯ β (π
1βsuc
π¦)} β (1o
β On β§ π₯ β
{β
, {β
}})) |
56 | 33, 55 | sylib 217 |
. . . . . . . 8
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β (1o
β On β§ π₯ β
{β
, {β
}})) |
57 | 12 | elpr 4609 |
. . . . . . . . . 10
β’ (π₯ β {β
, {β
}}
β (π₯ = β
β¨
π₯ =
{β
})) |
58 | | df-ne 2944 |
. . . . . . . . . . . 12
β’ (π₯ β β
β Β¬ π₯ = β
) |
59 | | orel1 887 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ = β
β ((π₯ = β
β¨ π₯ = {β
}) β π₯ = {β
})) |
60 | 58, 59 | sylbi 216 |
. . . . . . . . . . 11
β’ (π₯ β β
β ((π₯ = β
β¨ π₯ = {β
}) β π₯ = {β
})) |
61 | | df1o2 8419 |
. . . . . . . . . . . . 13
β’
1o = {β
} |
62 | | eqeq2 2748 |
. . . . . . . . . . . . 13
β’ (π₯ = {β
} β
(1o = π₯ β
1o = {β
})) |
63 | 61, 62 | mpbiri 257 |
. . . . . . . . . . . 12
β’ (π₯ = {β
} β
1o = π₯) |
64 | 63 | eqcomd 2742 |
. . . . . . . . . . 11
β’ (π₯ = {β
} β π₯ =
1o) |
65 | 60, 64 | syl6com 37 |
. . . . . . . . . 10
β’ ((π₯ = β
β¨ π₯ = {β
}) β (π₯ β β
β π₯ =
1o)) |
66 | 57, 65 | sylbi 216 |
. . . . . . . . 9
β’ (π₯ β {β
, {β
}}
β (π₯ β β
β π₯ =
1o)) |
67 | 66 | adantl 482 |
. . . . . . . 8
β’
((1o β On β§ π₯ β {β
, {β
}}) β (π₯ β β
β π₯ =
1o)) |
68 | 56, 67 | syl 17 |
. . . . . . 7
β’ (β© {π¦
β On β£ π₯ β
(π
1βsuc π¦)} = 1o β (π₯ β β
β π₯ = 1o)) |
69 | 17, 68 | sylbi 216 |
. . . . . 6
β’
((rankβπ₯) =
1o β (π₯
β β
β π₯ =
1o)) |
70 | 15, 69 | mpd 15 |
. . . . 5
β’
((rankβπ₯) =
1o β π₯ =
1o) |
71 | 9, 70 | vtoclg 3525 |
. . . 4
β’ (π΄ β V β
((rankβπ΄) =
1o β π΄ =
1o)) |
72 | 6, 71 | mpcom 38 |
. . 3
β’
((rankβπ΄) =
1o β π΄ =
1o) |
73 | | fveq2 6842 |
. . . 4
β’ (π΄ = 1o β
(rankβπ΄) =
(rankβ1o)) |
74 | | r111 9711 |
. . . . . . 7
β’
π
1:Onβ1-1βV |
75 | | f1dm 6742 |
. . . . . . 7
β’
(π
1:Onβ1-1βV β dom π
1 =
On) |
76 | 74, 75 | ax-mp 5 |
. . . . . 6
β’ dom
π
1 = On |
77 | 49, 76 | eleqtrri 2836 |
. . . . 5
β’
1o β dom π
1 |
78 | | rankonid 9765 |
. . . . 5
β’
(1o β dom π
1 β
(rankβ1o) = 1o) |
79 | 77, 78 | mpbi 229 |
. . . 4
β’
(rankβ1o) = 1o |
80 | 73, 79 | eqtrdi 2792 |
. . 3
β’ (π΄ = 1o β
(rankβπ΄) =
1o) |
81 | 72, 80 | impbii 208 |
. 2
β’
((rankβπ΄) =
1o β π΄ =
1o) |
82 | 61 | eqeq2i 2749 |
. 2
β’ (π΄ = 1o β π΄ = {β
}) |
83 | 81, 82 | bitri 274 |
1
β’
((rankβπ΄) =
1o β π΄ =
{β
}) |