Description: An alternate representation of a successor aleph. Compare alephsuc and alephsuc2 . Equality can be obtained by taking the card of the right-hand side then using alephcard and carden . (Contributed by NM, 23-Oct-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | alephsuc3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alephsuc2 | |
|
2 | alephcard | |
|
3 | alephon | |
|
4 | onenon | |
|
5 | 3 4 | ax-mp | |
6 | cardval2 | |
|
7 | 5 6 | ax-mp | |
8 | 2 7 | eqtr3i | |
9 | 8 | a1i | |
10 | 1 9 | difeq12d | |
11 | difrab | |
|
12 | bren2 | |
|
13 | 12 | rabbii | |
14 | 11 13 | eqtr4i | |
15 | 10 14 | eqtr2di | |
16 | alephon | |
|
17 | onenon | |
|
18 | 16 17 | mp1i | |
19 | onsucb | |
|
20 | alephgeom | |
|
21 | 19 20 | bitri | |
22 | fvex | |
|
23 | ssdomg | |
|
24 | 22 23 | ax-mp | |
25 | 21 24 | sylbi | |
26 | alephordilem1 | |
|
27 | infdif | |
|
28 | 18 25 26 27 | syl3anc | |
29 | 15 28 | eqbrtrd | |
30 | 29 | ensymd | |