This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. Definition 2.6 of Schloeder p. 4. (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 )