Step | Hyp | Ref
| Expression |
1 | | alephon 10013 |
. . . . . . . 8
β’
(β΅βπ΄)
β On |
2 | | id 22 |
. . . . . . . . . 10
β’
((cardβπ΅) =
π΅ β (cardβπ΅) = π΅) |
3 | | cardon 9888 |
. . . . . . . . . 10
β’
(cardβπ΅)
β On |
4 | 2, 3 | eqeltrrdi 2843 |
. . . . . . . . 9
β’
((cardβπ΅) =
π΅ β π΅ β On) |
5 | | onenon 9893 |
. . . . . . . . 9
β’ (π΅ β On β π΅ β dom
card) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’
((cardβπ΅) =
π΅ β π΅ β dom card) |
7 | | cardsdomel 9918 |
. . . . . . . 8
β’
(((β΅βπ΄)
β On β§ π΅ β
dom card) β ((β΅βπ΄) βΊ π΅ β (β΅βπ΄) β (cardβπ΅))) |
8 | 1, 6, 7 | sylancr 588 |
. . . . . . 7
β’
((cardβπ΅) =
π΅ β
((β΅βπ΄) βΊ
π΅ β
(β΅βπ΄) β
(cardβπ΅))) |
9 | | eleq2 2823 |
. . . . . . 7
β’
((cardβπ΅) =
π΅ β
((β΅βπ΄) β
(cardβπ΅) β
(β΅βπ΄) β
π΅)) |
10 | 8, 9 | bitrd 279 |
. . . . . 6
β’
((cardβπ΅) =
π΅ β
((β΅βπ΄) βΊ
π΅ β
(β΅βπ΄) β
π΅)) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((π΄ β On β§
(cardβπ΅) = π΅) β ((β΅βπ΄) βΊ π΅ β (β΅βπ΄) β π΅)) |
12 | | alephsuc 10012 |
. . . . . . . . . . 11
β’ (π΄ β On β
(β΅βsuc π΄) =
(harβ(β΅βπ΄))) |
13 | | onenon 9893 |
. . . . . . . . . . . 12
β’
((β΅βπ΄)
β On β (β΅βπ΄) β dom card) |
14 | | harval2 9941 |
. . . . . . . . . . . 12
β’
((β΅βπ΄)
β dom card β (harβ(β΅βπ΄)) = β© {π₯ β On β£
(β΅βπ΄) βΊ
π₯}) |
15 | 1, 13, 14 | mp2b 10 |
. . . . . . . . . . 11
β’
(harβ(β΅βπ΄)) = β© {π₯ β On β£
(β΅βπ΄) βΊ
π₯} |
16 | 12, 15 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π΄ β On β
(β΅βsuc π΄) =
β© {π₯ β On β£ (β΅βπ΄) βΊ π₯}) |
17 | 16 | eleq2d 2820 |
. . . . . . . . 9
β’ (π΄ β On β (π΅ β (β΅βsuc π΄) β π΅ β β© {π₯ β On β£
(β΅βπ΄) βΊ
π₯})) |
18 | 17 | biimpd 228 |
. . . . . . . 8
β’ (π΄ β On β (π΅ β (β΅βsuc π΄) β π΅ β β© {π₯ β On β£
(β΅βπ΄) βΊ
π₯})) |
19 | | breq2 5113 |
. . . . . . . . 9
β’ (π₯ = π΅ β ((β΅βπ΄) βΊ π₯ β (β΅βπ΄) βΊ π΅)) |
20 | 19 | onnminsb 7738 |
. . . . . . . 8
β’ (π΅ β On β (π΅ β β© {π₯
β On β£ (β΅βπ΄) βΊ π₯} β Β¬ (β΅βπ΄) βΊ π΅)) |
21 | 18, 20 | sylan9 509 |
. . . . . . 7
β’ ((π΄ β On β§ π΅ β On) β (π΅ β (β΅βsuc π΄) β Β¬
(β΅βπ΄) βΊ
π΅)) |
22 | 21 | con2d 134 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β
((β΅βπ΄) βΊ
π΅ β Β¬ π΅ β (β΅βsuc π΄))) |
23 | 4, 22 | sylan2 594 |
. . . . 5
β’ ((π΄ β On β§
(cardβπ΅) = π΅) β ((β΅βπ΄) βΊ π΅ β Β¬ π΅ β (β΅βsuc π΄))) |
24 | 11, 23 | sylbird 260 |
. . . 4
β’ ((π΄ β On β§
(cardβπ΅) = π΅) β ((β΅βπ΄) β π΅ β Β¬ π΅ β (β΅βsuc π΄))) |
25 | | imnan 401 |
. . . 4
β’
(((β΅βπ΄)
β π΅ β Β¬ π΅ β (β΅βsuc π΄)) β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄))) |
26 | 24, 25 | sylib 217 |
. . 3
β’ ((π΄ β On β§
(cardβπ΅) = π΅) β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄))) |
27 | 26 | ex 414 |
. 2
β’ (π΄ β On β
((cardβπ΅) = π΅ β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄)))) |
28 | | n0i 4297 |
. . . . . . 7
β’ (π΅ β (β΅βsuc π΄) β Β¬
(β΅βsuc π΄) =
β
) |
29 | | alephfnon 10009 |
. . . . . . . . . 10
β’ β΅
Fn On |
30 | 29 | fndmi 6610 |
. . . . . . . . 9
β’ dom
β΅ = On |
31 | 30 | eleq2i 2826 |
. . . . . . . 8
β’ (suc
π΄ β dom β΅ β
suc π΄ β
On) |
32 | | ndmfv 6881 |
. . . . . . . 8
β’ (Β¬
suc π΄ β dom β΅
β (β΅βsuc π΄) = β
) |
33 | 31, 32 | sylnbir 331 |
. . . . . . 7
β’ (Β¬
suc π΄ β On β
(β΅βsuc π΄) =
β
) |
34 | 28, 33 | nsyl2 141 |
. . . . . 6
β’ (π΅ β (β΅βsuc π΄) β suc π΄ β On) |
35 | | onsucb 7756 |
. . . . . 6
β’ (π΄ β On β suc π΄ β On) |
36 | 34, 35 | sylibr 233 |
. . . . 5
β’ (π΅ β (β΅βsuc π΄) β π΄ β On) |
37 | 36 | adantl 483 |
. . . 4
β’
(((β΅βπ΄)
β π΅ β§ π΅ β (β΅βsuc π΄)) β π΄ β On) |
38 | 37 | con3i 154 |
. . 3
β’ (Β¬
π΄ β On β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄))) |
39 | 38 | a1d 25 |
. 2
β’ (Β¬
π΄ β On β
((cardβπ΅) = π΅ β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄)))) |
40 | 27, 39 | pm2.61i 182 |
1
β’
((cardβπ΅) =
π΅ β Β¬
((β΅βπ΄) β
π΅ β§ π΅ β (β΅βsuc π΄))) |