Step | Hyp | Ref
| Expression |
1 | | alephsuc2 10077 |
. . . . 5
β’ (π΄ β On β
(β΅βsuc π΄) =
{π₯ β On β£ π₯ βΌ (β΅βπ΄)}) |
2 | | alephcard 10067 |
. . . . . . 7
β’
(cardβ(β΅βπ΄)) = (β΅βπ΄) |
3 | | alephon 10066 |
. . . . . . . . 9
β’
(β΅βπ΄)
β On |
4 | | onenon 9946 |
. . . . . . . . 9
β’
((β΅βπ΄)
β On β (β΅βπ΄) β dom card) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
β’
(β΅βπ΄)
β dom card |
6 | | cardval2 9988 |
. . . . . . . 8
β’
((β΅βπ΄)
β dom card β (cardβ(β΅βπ΄)) = {π₯ β On β£ π₯ βΊ (β΅βπ΄)}) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
β’
(cardβ(β΅βπ΄)) = {π₯ β On β£ π₯ βΊ (β΅βπ΄)} |
8 | 2, 7 | eqtr3i 2756 |
. . . . . 6
β’
(β΅βπ΄) =
{π₯ β On β£ π₯ βΊ (β΅βπ΄)} |
9 | 8 | a1i 11 |
. . . . 5
β’ (π΄ β On β
(β΅βπ΄) = {π₯ β On β£ π₯ βΊ (β΅βπ΄)}) |
10 | 1, 9 | difeq12d 4118 |
. . . 4
β’ (π΄ β On β
((β΅βsuc π΄)
β (β΅βπ΄))
= ({π₯ β On β£
π₯ βΌ
(β΅βπ΄)} β
{π₯ β On β£ π₯ βΊ (β΅βπ΄)})) |
11 | | difrab 4303 |
. . . . 5
β’ ({π₯ β On β£ π₯ βΌ (β΅βπ΄)} β {π₯ β On β£ π₯ βΊ (β΅βπ΄)}) = {π₯ β On β£ (π₯ βΌ (β΅βπ΄) β§ Β¬ π₯ βΊ (β΅βπ΄))} |
12 | | bren2 8981 |
. . . . . 6
β’ (π₯ β (β΅βπ΄) β (π₯ βΌ (β΅βπ΄) β§ Β¬ π₯ βΊ (β΅βπ΄))) |
13 | 12 | rabbii 3432 |
. . . . 5
β’ {π₯ β On β£ π₯ β (β΅βπ΄)} = {π₯ β On β£ (π₯ βΌ (β΅βπ΄) β§ Β¬ π₯ βΊ (β΅βπ΄))} |
14 | 11, 13 | eqtr4i 2757 |
. . . 4
β’ ({π₯ β On β£ π₯ βΌ (β΅βπ΄)} β {π₯ β On β£ π₯ βΊ (β΅βπ΄)}) = {π₯ β On β£ π₯ β (β΅βπ΄)} |
15 | 10, 14 | eqtr2di 2783 |
. . 3
β’ (π΄ β On β {π₯ β On β£ π₯ β (β΅βπ΄)} = ((β΅βsuc π΄) β (β΅βπ΄))) |
16 | | alephon 10066 |
. . . . 5
β’
(β΅βsuc π΄) β On |
17 | | onenon 9946 |
. . . . 5
β’
((β΅βsuc π΄) β On β (β΅βsuc π΄) β dom
card) |
18 | 16, 17 | mp1i 13 |
. . . 4
β’ (π΄ β On β
(β΅βsuc π΄)
β dom card) |
19 | | onsucb 7802 |
. . . . . 6
β’ (π΄ β On β suc π΄ β On) |
20 | | alephgeom 10079 |
. . . . . 6
β’ (suc
π΄ β On β Ο
β (β΅βsuc π΄)) |
21 | 19, 20 | bitri 275 |
. . . . 5
β’ (π΄ β On β Ο
β (β΅βsuc π΄)) |
22 | | fvex 6898 |
. . . . . 6
β’
(β΅βsuc π΄) β V |
23 | | ssdomg 8998 |
. . . . . 6
β’
((β΅βsuc π΄) β V β (Ο β
(β΅βsuc π΄)
β Ο βΌ (β΅βsuc π΄))) |
24 | 22, 23 | ax-mp 5 |
. . . . 5
β’ (Ο
β (β΅βsuc π΄) β Ο βΌ (β΅βsuc
π΄)) |
25 | 21, 24 | sylbi 216 |
. . . 4
β’ (π΄ β On β Ο
βΌ (β΅βsuc π΄)) |
26 | | alephordilem1 10070 |
. . . 4
β’ (π΄ β On β
(β΅βπ΄) βΊ
(β΅βsuc π΄)) |
27 | | infdif 10206 |
. . . 4
β’
(((β΅βsuc π΄) β dom card β§ Ο βΌ
(β΅βsuc π΄) β§
(β΅βπ΄) βΊ
(β΅βsuc π΄))
β ((β΅βsuc π΄) β (β΅βπ΄)) β (β΅βsuc π΄)) |
28 | 18, 25, 26, 27 | syl3anc 1368 |
. . 3
β’ (π΄ β On β
((β΅βsuc π΄)
β (β΅βπ΄))
β (β΅βsuc π΄)) |
29 | 15, 28 | eqbrtrd 5163 |
. 2
β’ (π΄ β On β {π₯ β On β£ π₯ β (β΅βπ΄)} β (β΅βsuc
π΄)) |
30 | 29 | ensymd 9003 |
1
β’ (π΄ β On β
(β΅βsuc π΄)
β {π₯ β On
β£ π₯ β
(β΅βπ΄)}) |