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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o ∅ ) )
2 oe0m0 ⊢ ( ∅ ↑o ∅ ) = 1o
3 1 2 eqtrdi ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = 1o )
4 fveq2 ⊢ ( 𝐵 = ∅ → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ ∅ ) )
5 1oex ⊢ 1o ∈ V
6 5 rdg0 ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ ∅ ) = 1o
7 4 6 eqtrdi ⊢ ( 𝐵 = ∅ → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = 1o )
8 inteq ⊢ ( 𝐵 = ∅ → ∩ 𝐵 = ∩ ∅ )
9 int0 ⊢ ∩ ∅ = V
10 8 9 eqtrdi ⊢ ( 𝐵 = ∅ → ∩ 𝐵 = V )
11 7 10 ineq12d ⊢ ( 𝐵 = ∅ → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) = ( 1o ∩ V ) )
12 inv1 ⊢ ( 1o ∩ V ) = 1o
13 12 a1i ⊢ ( 𝐴 = ∅ → ( 1o ∩ V ) = 1o )
14 11 13 sylan9eqr ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) = 1o )
15 3 14 eqtr4d ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) )
16 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
17 oe0m1 ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
18 17 biimpa ⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
19 16 18 sylan9eqr ⊢ ( ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ∅ )
20 19 an32s ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) ∧ ∅ ∈ 𝐵 ) → ( 𝐴 ↑o 𝐵 ) = ∅ )
21 int0el ⊢ ( ∅ ∈ 𝐵 → ∩ 𝐵 = ∅ )
22 21 ineq2d ⊢ ( ∅ ∈ 𝐵 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∅ ) )
23 in0 ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∅ ) = ∅
24 22 23 eqtrdi ⊢ ( ∅ ∈ 𝐵 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) = ∅ )
25 24 adantl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) ∧ ∅ ∈ 𝐵 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) = ∅ )
26 20 25 eqtr4d ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) ∧ ∅ ∈ 𝐵 ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) )
27 15 26 oe0lem ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) )
28 inteq ⊢ ( 𝐴 = ∅ → ∩ 𝐴 = ∩ ∅ )
29 28 9 eqtrdi ⊢ ( 𝐴 = ∅ → ∩ 𝐴 = V )
30 29 difeq2d ⊢ ( 𝐴 = ∅ → ( V ∖ ∩ 𝐴 ) = ( V ∖ V ) )
31 difid ⊢ ( V ∖ V ) = ∅
32 30 31 eqtrdi ⊢ ( 𝐴 = ∅ → ( V ∖ ∩ 𝐴 ) = ∅ )
33 32 uneq2d ⊢ ( 𝐴 = ∅ → ( ∩ 𝐵 ∪ ( V ∖ ∩ 𝐴 ) ) = ( ∩ 𝐵 ∪ ∅ ) )
34 uncom ⊢ ( ∩ 𝐵 ∪ ( V ∖ ∩ 𝐴 ) ) = ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 )
35 un0 ⊢ ( ∩ 𝐵 ∪ ∅ ) = ∩ 𝐵
36 33 34 35 3eqtr3g ⊢ ( 𝐴 = ∅ → ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) = ∩ 𝐵 )
37 36 adantl ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) = ∩ 𝐵 )
38 37 ineq2d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ∩ 𝐵 ) )
39 27 38 eqtr4d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) )
40 oevn0 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )
41 int0el ⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 = ∅ )
42 41 difeq2d ⊢ ( ∅ ∈ 𝐴 → ( V ∖ ∩ 𝐴 ) = ( V ∖ ∅ ) )
43 dif0 ⊢ ( V ∖ ∅ ) = V
44 42 43 eqtrdi ⊢ ( ∅ ∈ 𝐴 → ( V ∖ ∩ 𝐴 ) = V )
45 44 uneq2d ⊢ ( ∅ ∈ 𝐴 → ( ∩ 𝐵 ∪ ( V ∖ ∩ 𝐴 ) ) = ( ∩ 𝐵 ∪ V ) )
46 unv ⊢ ( ∩ 𝐵 ∪ V ) = V
47 45 34 46 3eqtr3g ⊢ ( ∅ ∈ 𝐴 → ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) = V )
48 47 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) = V )
49 48 ineq2d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ V ) )
50 inv1 ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ V ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 )
51 49 50 eqtr2di ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) )
52 40 51 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) )
53 39 52 oe0lem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ∩ ( ( V ∖ ∩ 𝐴 ) ∪ ∩ 𝐵 ) ) )