Metamath Proof Explorer


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 ) ‘ 𝐵 ) )