Theorem oevn0

Description: Value of ordinal exponentiation at a nonzero base. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	oevn0	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
2		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
3	1 2	bitrdi	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ¬ 𝐴 = ∅ ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 ↔ ¬ 𝐴 = ∅ ) )
5		oev	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = if ( 𝐴 = ∅ , ( 1o ∖ 𝐵 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
6		iffalse	⊢ ( ¬ 𝐴 = ∅ → if ( 𝐴 = ∅ , ( 1o ∖ 𝐵 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )
7	5 6	sylan9eq	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )
8	7	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
9	4 8	sylbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
10	9	imp	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )