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 )