Metamath Proof Explorer


Theorem oev2

Description: Alternate value of ordinal exponentiation. Compare oev . (Contributed by NM, 2-Jan-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oev2 A On B On A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B V A B

Proof

Step Hyp Ref Expression
1 oveq12 A = B = A 𝑜 B = 𝑜
2 oe0m0 𝑜 = 1 𝑜
3 1 2 eqtrdi A = B = A 𝑜 B = 1 𝑜
4 fveq2 B = rec x V x 𝑜 A 1 𝑜 B = rec x V x 𝑜 A 1 𝑜
5 1oex 1 𝑜 V
6 5 rdg0 rec x V x 𝑜 A 1 𝑜 = 1 𝑜
7 4 6 eqtrdi B = rec x V x 𝑜 A 1 𝑜 B = 1 𝑜
8 inteq B = B =
9 int0 = V
10 8 9 eqtrdi B = B = V
11 7 10 ineq12d B = rec x V x 𝑜 A 1 𝑜 B B = 1 𝑜 V
12 inv1 1 𝑜 V = 1 𝑜
13 12 a1i A = 1 𝑜 V = 1 𝑜
14 11 13 sylan9eqr A = B = rec x V x 𝑜 A 1 𝑜 B B = 1 𝑜
15 3 14 eqtr4d A = B = A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B B
16 oveq1 A = A 𝑜 B = 𝑜 B
17 oe0m1 B On B 𝑜 B =
18 17 biimpa B On B 𝑜 B =
19 16 18 sylan9eqr B On B A = A 𝑜 B =
20 19 an32s B On A = B A 𝑜 B =
21 int0el B B =
22 21 ineq2d B rec x V x 𝑜 A 1 𝑜 B B = rec x V x 𝑜 A 1 𝑜 B
23 in0 rec x V x 𝑜 A 1 𝑜 B =
24 22 23 eqtrdi B rec x V x 𝑜 A 1 𝑜 B B =
25 24 adantl B On A = B rec x V x 𝑜 A 1 𝑜 B B =
26 20 25 eqtr4d B On A = B A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B B
27 15 26 oe0lem B On A = A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B B
28 inteq A = A =
29 28 9 eqtrdi A = A = V
30 29 difeq2d A = V A = V V
31 difid V V =
32 30 31 eqtrdi A = V A =
33 32 uneq2d A = B V A = B
34 uncom B V A = V A B
35 un0 B = B
36 33 34 35 3eqtr3g A = V A B = B
37 36 adantl B On A = V A B = B
38 37 ineq2d B On A = rec x V x 𝑜 A 1 𝑜 B V A B = rec x V x 𝑜 A 1 𝑜 B B
39 27 38 eqtr4d B On A = A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B V A B
40 oevn0 A On B On A A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B
41 int0el A A =
42 41 difeq2d A V A = V
43 dif0 V = V
44 42 43 eqtrdi A V A = V
45 44 uneq2d A B V A = B V
46 unv B V = V
47 45 34 46 3eqtr3g A V A B = V
48 47 adantl A On B On A V A B = V
49 48 ineq2d A On B On A rec x V x 𝑜 A 1 𝑜 B V A B = rec x V x 𝑜 A 1 𝑜 B V
50 inv1 rec x V x 𝑜 A 1 𝑜 B V = rec x V x 𝑜 A 1 𝑜 B
51 49 50 eqtr2di A On B On A rec x V x 𝑜 A 1 𝑜 B = rec x V x 𝑜 A 1 𝑜 B V A B
52 40 51 eqtrd A On B On A A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B V A B
53 39 52 oe0lem A On B On A 𝑜 B = rec x V x 𝑜 A 1 𝑜 B V A B