Description: Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | iscard | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cardon | |
|
2 | eleq1 | |
|
3 | 1 2 | mpbii | |
4 | cardonle | |
|
5 | eqss | |
|
6 | 5 | baibr | |
7 | 4 6 | syl | |
8 | dfss3 | |
|
9 | onelon | |
|
10 | onenon | |
|
11 | 10 | adantr | |
12 | cardsdomel | |
|
13 | 9 11 12 | syl2anc | |
14 | 13 | ralbidva | |
15 | 8 14 | bitr4id | |
16 | 7 15 | bitr3d | |
17 | 3 16 | biadanii | |