Description: A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | coflim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | |
|
2 | 1 | biimprd | |
3 | eluni2 | |
|
4 | limord | |
|
5 | ssel2 | |
|
6 | ordelon | |
|
7 | 4 5 6 | syl2an | |
8 | 7 | expr | |
9 | onelss | |
|
10 | 8 9 | syl6 | |
11 | 10 | reximdvai | |
12 | 3 11 | syl5bi | |
13 | 2 12 | syl9r | |
14 | 13 | ralrimdv | |
15 | uniss | |
|
16 | 15 | 3ad2ant2 | |
17 | uniss2 | |
|
18 | 17 | 3ad2ant3 | |
19 | 16 18 | eqssd | |
20 | limuni | |
|
21 | 20 | 3ad2ant1 | |
22 | 19 21 | eqtr4d | |
23 | 22 | 3expia | |
24 | 14 23 | impbid | |