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

Metamath Proof Explorer

Theorem oev

Description: Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004) (Revised by Mario Carneiro, 23-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 = ∅ ↔ 𝐴 = ∅ ) )
2 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ·o 𝑦 ) = ( 𝑥 ·o 𝐴 ) )
3 2 mpteq2dv ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) )
4 rdgeq1 ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) , 1o ) = rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) )
5 3 4 syl ⊢ ( 𝑦 = 𝐴 → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) , 1o ) = rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) )
6 5 fveq1d ⊢ ( 𝑦 = 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) , 1o ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝑧 ) )
7 1 6 ifbieq2d ⊢ ( 𝑦 = 𝐴 → if ( 𝑦 = ∅ , ( 1o ∖ 𝑧 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) , 1o ) ‘ 𝑧 ) ) = if ( 𝐴 = ∅ , ( 1o ∖ 𝑧 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝑧 ) ) )
8 difeq2 ⊢ ( 𝑧 = 𝐵 → ( 1o ∖ 𝑧 ) = ( 1o ∖ 𝐵 ) )
9 fveq2 ⊢ ( 𝑧 = 𝐵 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )
10 8 9 ifeq12d ⊢ ( 𝑧 = 𝐵 → if ( 𝐴 = ∅ , ( 1o ∖ 𝑧 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝑧 ) ) = if ( 𝐴 = ∅ , ( 1o ∖ 𝐵 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
11 df-oexp ⊢ ↑o = ( 𝑦 ∈ On , 𝑧 ∈ On ↦ if ( 𝑦 = ∅ , ( 1o ∖ 𝑧 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝑦 ) ) , 1o ) ‘ 𝑧 ) ) )
12 1oex ⊢ 1o ∈ V
13 12 difexi ⊢ ( 1o ∖ 𝐵 ) ∈ V
14 fvex ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∈ V
15 13 14 ifex ⊢ if ( 𝐴 = ∅ , ( 1o ∖ 𝐵 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ∈ V
16 7 10 11 15 ovmpo ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = if ( 𝐴 = ∅ , ( 1o ∖ 𝐵 ) , ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )