Metamath Proof Explorer


Theorem oe0m

Description: Value of zero raised to an ordinal. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oe0m ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o𝐴 ) )

Proof

Step Hyp Ref Expression
1 0elon ∅ ∈ On
2 oev ( ( ∅ ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ↑o 𝐴 ) = if ( ∅ = ∅ , ( 1o𝐴 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o ∅ ) ) , 1o ) ‘ 𝐴 ) ) )
3 1 2 mpan ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = if ( ∅ = ∅ , ( 1o𝐴 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o ∅ ) ) , 1o ) ‘ 𝐴 ) ) )
4 eqid ∅ = ∅
5 4 iftruei if ( ∅ = ∅ , ( 1o𝐴 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o ∅ ) ) , 1o ) ‘ 𝐴 ) ) = ( 1o𝐴 )
6 3 5 eqtrdi ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o𝐴 ) )