Description: An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | unizlim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne | |
|
2 | df-lim | |
|
3 | 2 | biimpri | |
4 | 3 | 3exp | |
5 | 1 4 | syl5bir | |
6 | 5 | com23 | |
7 | 6 | imp | |
8 | 7 | orrd | |
9 | 8 | ex | |
10 | uni0 | |
|
11 | 10 | eqcomi | |
12 | id | |
|
13 | unieq | |
|
14 | 11 12 13 | 3eqtr4a | |
15 | limuni | |
|
16 | 14 15 | jaoi | |
17 | 9 16 | impbid1 | |