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 A On B On A 𝑜 B = if A = 1 𝑜 B rec x V x 𝑜 A 1 𝑜 B

Proof

Step Hyp Ref Expression
1 eqeq1 y = A y = A =
2 oveq2 y = A x 𝑜 y = x 𝑜 A
3 2 mpteq2dv y = A x V x 𝑜 y = x V x 𝑜 A
4 rdgeq1 x V x 𝑜 y = x V x 𝑜 A rec x V x 𝑜 y 1 𝑜 = rec x V x 𝑜 A 1 𝑜
5 3 4 syl y = A rec x V x 𝑜 y 1 𝑜 = rec x V x 𝑜 A 1 𝑜
6 5 fveq1d y = A rec x V x 𝑜 y 1 𝑜 z = rec x V x 𝑜 A 1 𝑜 z
7 1 6 ifbieq2d y = A if y = 1 𝑜 z rec x V x 𝑜 y 1 𝑜 z = if A = 1 𝑜 z rec x V x 𝑜 A 1 𝑜 z
8 difeq2 z = B 1 𝑜 z = 1 𝑜 B
9 fveq2 z = B rec x V x 𝑜 A 1 𝑜 z = rec x V x 𝑜 A 1 𝑜 B
10 8 9 ifeq12d z = B if A = 1 𝑜 z rec x V x 𝑜 A 1 𝑜 z = if A = 1 𝑜 B rec x V x 𝑜 A 1 𝑜 B
11 df-oexp 𝑜 = y On , z On if y = 1 𝑜 z rec x V x 𝑜 y 1 𝑜 z
12 1oex 1 𝑜 V
13 12 difexi 1 𝑜 B V
14 fvex rec x V x 𝑜 A 1 𝑜 B V
15 13 14 ifex if A = 1 𝑜 B rec x V x 𝑜 A 1 𝑜 B V
16 7 10 11 15 ovmpo A On B On A 𝑜 B = if A = 1 𝑜 B rec x V x 𝑜 A 1 𝑜 B