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 syl6eq ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴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 syl6eq ( 𝐵 = ∅ → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = 1o )
8 inteq ( 𝐵 = ∅ → 𝐵 = ∅ )
9 int0 ∅ = V
10 8 9 syl6eq ( 𝐵 = ∅ → 𝐵 = 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 syl6eq ( ∅ ∈ 𝐵 → ( ( 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 syl6eq ( 𝐴 = ∅ → 𝐴 = V )
30 29 difeq2d ( 𝐴 = ∅ → ( V ∖ 𝐴 ) = ( V ∖ V ) )
31 difid ( V ∖ V ) = ∅
32 30 31 syl6eq ( 𝐴 = ∅ → ( 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 syl6eq ( ∅ ∈ 𝐴 → ( 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 syl6req ( ( ( 𝐴 ∈ 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 ∖ 𝐴 ) ∪ 𝐵 ) ) )