Metamath Proof Explorer


Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝐴 = ∅ → ( 𝐴o ∅ ) = ( ∅ ↑o ∅ ) )
2 oe0m0 ( ∅ ↑o ∅ ) = 1o
3 1 2 eqtrdi ( 𝐴 = ∅ → ( 𝐴o ∅ ) = 1o )
4 3 adantl ( ( 𝐴 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴o ∅ ) = 1o )
5 0elon ∅ ∈ On
6 oevn0 ( ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ ∅ ) )
7 5 6 mpanl2 ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝐴o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ ∅ ) )
8 1oex 1o ∈ V
9 8 rdg0 ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ ∅ ) = 1o
10 7 9 eqtrdi ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝐴o ∅ ) = 1o )
11 10 adantll ( ( ( 𝐴 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴o ∅ ) = 1o )
12 4 11 oe0lem ( ( 𝐴 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐴o ∅ ) = 1o )
13 12 anidms ( 𝐴 ∈ On → ( 𝐴o ∅ ) = 1o )