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