Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
β’ (π΄ β β
β Β¬ π΄ = β
) |
2 | | simplr 768 |
. . . . . . . . . 10
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β
(π
1βπ΄) β Tarski) |
3 | | simpll 766 |
. . . . . . . . . 10
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β π΄ β On) |
4 | | onwf 9774 |
. . . . . . . . . . . . . . . 16
β’ On
β βͺ (π
1 β
On) |
5 | 4 | sseli 3944 |
. . . . . . . . . . . . . . 15
β’ (π΄ β On β π΄ β βͺ (π
1 β On)) |
6 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(rankβπ΄) =
(rankβπ΄) |
7 | | rankr1c 9765 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β βͺ (π
1 β On) β
((rankβπ΄) =
(rankβπ΄) β
(Β¬ π΄ β
(π
1β(rankβπ΄)) β§ π΄ β (π
1βsuc
(rankβπ΄))))) |
8 | 6, 7 | mpbii 232 |
. . . . . . . . . . . . . . 15
β’ (π΄ β βͺ (π
1 β On) β (Β¬ π΄ β
(π
1β(rankβπ΄)) β§ π΄ β (π
1βsuc
(rankβπ΄)))) |
9 | 5, 8 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΄ β On β (Β¬ π΄ β
(π
1β(rankβπ΄)) β§ π΄ β (π
1βsuc
(rankβπ΄)))) |
10 | 9 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π΄ β On β Β¬ π΄ β
(π
1β(rankβπ΄))) |
11 | | r1fnon 9711 |
. . . . . . . . . . . . . . . . 17
β’
π
1 Fn On |
12 | 11 | fndmi 6610 |
. . . . . . . . . . . . . . . 16
β’ dom
π
1 = On |
13 | 12 | eleq2i 2826 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom
π
1 β π΄ β On) |
14 | | rankonid 9773 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom
π
1 β (rankβπ΄) = π΄) |
15 | 13, 14 | bitr3i 277 |
. . . . . . . . . . . . . 14
β’ (π΄ β On β
(rankβπ΄) = π΄) |
16 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’
((rankβπ΄) =
π΄ β
(π
1β(rankβπ΄)) = (π
1βπ΄)) |
17 | 15, 16 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (π΄ β On β
(π
1β(rankβπ΄)) = (π
1βπ΄)) |
18 | 10, 17 | neleqtrd 2856 |
. . . . . . . . . . . 12
β’ (π΄ β On β Β¬ π΄ β
(π
1βπ΄)) |
19 | 18 | adantl 483 |
. . . . . . . . . . 11
β’
(((π
1βπ΄) β Tarski β§ π΄ β On) β Β¬ π΄ β (π
1βπ΄)) |
20 | | onssr1 9775 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom
π
1 β π΄ β (π
1βπ΄)) |
21 | 13, 20 | sylbir 234 |
. . . . . . . . . . . . 13
β’ (π΄ β On β π΄ β
(π
1βπ΄)) |
22 | | tsken 10698 |
. . . . . . . . . . . . 13
β’
(((π
1βπ΄) β Tarski β§ π΄ β (π
1βπ΄)) β (π΄ β (π
1βπ΄) β¨ π΄ β (π
1βπ΄))) |
23 | 21, 22 | sylan2 594 |
. . . . . . . . . . . 12
β’
(((π
1βπ΄) β Tarski β§ π΄ β On) β (π΄ β (π
1βπ΄) β¨ π΄ β (π
1βπ΄))) |
24 | 23 | ord 863 |
. . . . . . . . . . 11
β’
(((π
1βπ΄) β Tarski β§ π΄ β On) β (Β¬ π΄ β (π
1βπ΄) β π΄ β (π
1βπ΄))) |
25 | 19, 24 | mt3d 148 |
. . . . . . . . . 10
β’
(((π
1βπ΄) β Tarski β§ π΄ β On) β π΄ β (π
1βπ΄)) |
26 | 2, 3, 25 | syl2anc 585 |
. . . . . . . . 9
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β π΄ β (π
1βπ΄)) |
27 | | carden2b 9911 |
. . . . . . . . 9
β’ (π΄ β
(π
1βπ΄) β (cardβπ΄) =
(cardβ(π
1βπ΄))) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β (cardβπ΄) =
(cardβ(π
1βπ΄))) |
29 | | simpl 484 |
. . . . . . . . . 10
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β π΄ β On) |
30 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β (π
1βπ΄) β
Tarski) |
31 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β π΄ β (π
1βπ΄)) |
32 | 31 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β π₯ β (π
1βπ΄)) |
33 | | tsksdom 10700 |
. . . . . . . . . . . . 13
β’
(((π
1βπ΄) β Tarski β§ π₯ β (π
1βπ΄)) β π₯ βΊ (π
1βπ΄)) |
34 | 30, 32, 33 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β π₯ βΊ (π
1βπ΄)) |
35 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β π΄ β On) |
36 | 25 | ensymd 8951 |
. . . . . . . . . . . . 13
β’
(((π
1βπ΄) β Tarski β§ π΄ β On) β
(π
1βπ΄) β π΄) |
37 | 30, 35, 36 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β (π
1βπ΄) β π΄) |
38 | | sdomentr 9061 |
. . . . . . . . . . . 12
β’ ((π₯ βΊ
(π
1βπ΄) β§ (π
1βπ΄) β π΄) β π₯ βΊ π΄) |
39 | 34, 37, 38 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π₯ β π΄) β π₯ βΊ π΄) |
40 | 39 | ralrimiva 3140 |
. . . . . . . . . 10
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β βπ₯ β π΄ π₯ βΊ π΄) |
41 | | iscard 9919 |
. . . . . . . . . 10
β’
((cardβπ΄) =
π΄ β (π΄ β On β§ βπ₯ β π΄ π₯ βΊ π΄)) |
42 | 29, 40, 41 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β (cardβπ΄) = π΄) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β (cardβπ΄) = π΄) |
44 | 28, 43 | eqtr3d 2775 |
. . . . . . 7
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β
(cardβ(π
1βπ΄)) = π΄) |
45 | | r10 9712 |
. . . . . . . . . . 11
β’
(π
1ββ
) = β
|
46 | | on0eln0 6377 |
. . . . . . . . . . . . 13
β’ (π΄ β On β (β
β π΄ β π΄ β β
)) |
47 | 46 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ π΄ β β
) β β
β π΄) |
48 | | r1sdom 9718 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ β
β
π΄) β
(π
1ββ
) βΊ
(π
1βπ΄)) |
49 | 47, 48 | syldan 592 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π΄ β β
) β
(π
1ββ
) βΊ
(π
1βπ΄)) |
50 | 45, 49 | eqbrtrrid 5145 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΄ β β
) β β
βΊ (π
1βπ΄)) |
51 | | fvex 6859 |
. . . . . . . . . . 11
β’
(π
1βπ΄) β V |
52 | 51 | 0sdom 9057 |
. . . . . . . . . 10
β’ (β
βΊ (π
1βπ΄) β (π
1βπ΄) β β
) |
53 | 50, 52 | sylib 217 |
. . . . . . . . 9
β’ ((π΄ β On β§ π΄ β β
) β
(π
1βπ΄) β β
) |
54 | 53 | adantlr 714 |
. . . . . . . 8
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β
(π
1βπ΄) β β
) |
55 | | tskcard 10725 |
. . . . . . . 8
β’
(((π
1βπ΄) β Tarski β§
(π
1βπ΄) β β
) β
(cardβ(π
1βπ΄)) β Inacc) |
56 | 2, 54, 55 | syl2anc 585 |
. . . . . . 7
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β
(cardβ(π
1βπ΄)) β Inacc) |
57 | 44, 56 | eqeltrrd 2835 |
. . . . . 6
β’ (((π΄ β On β§
(π
1βπ΄) β Tarski) β§ π΄ β β
) β π΄ β Inacc) |
58 | 57 | ex 414 |
. . . . 5
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β (π΄ β β
β π΄ β Inacc)) |
59 | 1, 58 | biimtrrid 242 |
. . . 4
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β (Β¬ π΄ = β
β π΄ β Inacc)) |
60 | 59 | orrd 862 |
. . 3
β’ ((π΄ β On β§
(π
1βπ΄) β Tarski) β (π΄ = β
β¨ π΄ β Inacc)) |
61 | 60 | ex 414 |
. 2
β’ (π΄ β On β
((π
1βπ΄) β Tarski β (π΄ = β
β¨ π΄ β Inacc))) |
62 | | fveq2 6846 |
. . . . 5
β’ (π΄ = β
β
(π
1βπ΄) =
(π
1ββ
)) |
63 | 62, 45 | eqtrdi 2789 |
. . . 4
β’ (π΄ = β
β
(π
1βπ΄) = β
) |
64 | | 0tsk 10699 |
. . . 4
β’ β
β Tarski |
65 | 63, 64 | eqeltrdi 2842 |
. . 3
β’ (π΄ = β
β
(π
1βπ΄) β Tarski) |
66 | | inatsk 10722 |
. . 3
β’ (π΄ β Inacc β
(π
1βπ΄) β Tarski) |
67 | 65, 66 | jaoi 856 |
. 2
β’ ((π΄ = β
β¨ π΄ β Inacc) β
(π
1βπ΄) β Tarski) |
68 | 61, 67 | impbid1 224 |
1
β’ (π΄ β On β
((π
1βπ΄) β Tarski β (π΄ = β
β¨ π΄ β Inacc))) |