Description: Ordinal exponentiation with zero base and nonzero exponent. Proposition 8.31(2) of TakeutiZaring p. 67 and its converse. (Contributed by NM, 5-Jan-2005)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | oe0m1 | |- ( A e. On -> ( (/) e. A <-> ( (/) ^o A ) = (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eloni | |- ( A e. On -> Ord A ) |
|
| 2 | ordgt0ge1 | |- ( Ord A -> ( (/) e. A <-> 1o C_ A ) ) |
|
| 3 | 1 2 | syl | |- ( A e. On -> ( (/) e. A <-> 1o C_ A ) ) |
| 4 | ssdif0 | |- ( 1o C_ A <-> ( 1o \ A ) = (/) ) |
|
| 5 | oe0m | |- ( A e. On -> ( (/) ^o A ) = ( 1o \ A ) ) |
|
| 6 | 5 | eqeq1d | |- ( A e. On -> ( ( (/) ^o A ) = (/) <-> ( 1o \ A ) = (/) ) ) |
| 7 | 4 6 | bitr4id | |- ( A e. On -> ( 1o C_ A <-> ( (/) ^o A ) = (/) ) ) |
| 8 | 3 7 | bitrd | |- ( A e. On -> ( (/) e. A <-> ( (/) ^o A ) = (/) ) ) |