Metamath Proof Explorer


Theorem oe0m1

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 ) = (/) ) )

Proof

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 ) = (/) ) )