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 ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 eloni ( 𝐴 ∈ On → Ord 𝐴 )
2 ordgt0ge1 ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o𝐴 ) )
3 1 2 syl ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 1o𝐴 ) )
4 ssdif0 ( 1o𝐴 ↔ ( 1o𝐴 ) = ∅ )
5 oe0m ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o𝐴 ) )
6 5 eqeq1d ( 𝐴 ∈ On → ( ( ∅ ↑o 𝐴 ) = ∅ ↔ ( 1o𝐴 ) = ∅ ) )
7 4 6 bitr4id ( 𝐴 ∈ On → ( 1o𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )
8 3 7 bitrd ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )