Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | cardalephex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | cardaleph | |
|
3 | 2 | sseq2d | |
4 | alephgeom | |
|
5 | 3 4 | bitr4di | |
6 | 1 5 | mpbid | |
7 | fveq2 | |
|
8 | 7 | rspceeqv | |
9 | 6 2 8 | syl2anc | |
10 | 9 | ex | |
11 | alephcard | |
|
12 | fveq2 | |
|
13 | id | |
|
14 | 11 12 13 | 3eqtr4a | |
15 | 14 | rexlimivw | |
16 | 10 15 | impbid1 | |