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 e. On /\ B e. On ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )

Proof

Step Hyp Ref Expression
1 oveq12
 |-  ( ( A = (/) /\ B = (/) ) -> ( A ^o B ) = ( (/) ^o (/) ) )
2 oe0m0
 |-  ( (/) ^o (/) ) = 1o
3 1 2 eqtrdi
 |-  ( ( A = (/) /\ B = (/) ) -> ( A ^o B ) = 1o )
4 fveq2
 |-  ( B = (/) -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` (/) ) )
5 1oex
 |-  1o e. _V
6 5 rdg0
 |-  ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` (/) ) = 1o
7 4 6 eqtrdi
 |-  ( B = (/) -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) = 1o )
8 inteq
 |-  ( B = (/) -> |^| B = |^| (/) )
9 int0
 |-  |^| (/) = _V
10 8 9 eqtrdi
 |-  ( B = (/) -> |^| B = _V )
11 7 10 ineq12d
 |-  ( B = (/) -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) = ( 1o i^i _V ) )
12 inv1
 |-  ( 1o i^i _V ) = 1o
13 12 a1i
 |-  ( A = (/) -> ( 1o i^i _V ) = 1o )
14 11 13 sylan9eqr
 |-  ( ( A = (/) /\ B = (/) ) -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) = 1o )
15 3 14 eqtr4d
 |-  ( ( A = (/) /\ B = (/) ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) )
16 oveq1
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
17 oe0m1
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
18 17 biimpa
 |-  ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
19 16 18 sylan9eqr
 |-  ( ( ( B e. On /\ (/) e. B ) /\ A = (/) ) -> ( A ^o B ) = (/) )
20 19 an32s
 |-  ( ( ( B e. On /\ A = (/) ) /\ (/) e. B ) -> ( A ^o B ) = (/) )
21 int0el
 |-  ( (/) e. B -> |^| B = (/) )
22 21 ineq2d
 |-  ( (/) e. B -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i (/) ) )
23 in0
 |-  ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i (/) ) = (/)
24 22 23 eqtrdi
 |-  ( (/) e. B -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) = (/) )
25 24 adantl
 |-  ( ( ( B e. On /\ A = (/) ) /\ (/) e. B ) -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) = (/) )
26 20 25 eqtr4d
 |-  ( ( ( B e. On /\ A = (/) ) /\ (/) e. B ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) )
27 15 26 oe0lem
 |-  ( ( B e. On /\ A = (/) ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| 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 u. ( _V \ |^| A ) ) = ( |^| B u. (/) ) )
34 uncom
 |-  ( |^| B u. ( _V \ |^| A ) ) = ( ( _V \ |^| A ) u. |^| B )
35 un0
 |-  ( |^| B u. (/) ) = |^| B
36 33 34 35 3eqtr3g
 |-  ( A = (/) -> ( ( _V \ |^| A ) u. |^| B ) = |^| B )
37 36 adantl
 |-  ( ( B e. On /\ A = (/) ) -> ( ( _V \ |^| A ) u. |^| B ) = |^| B )
38 37 ineq2d
 |-  ( ( B e. On /\ A = (/) ) -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i |^| B ) )
39 27 38 eqtr4d
 |-  ( ( B e. On /\ A = (/) ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )
40 oevn0
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
41 int0el
 |-  ( (/) e. A -> |^| A = (/) )
42 41 difeq2d
 |-  ( (/) e. A -> ( _V \ |^| A ) = ( _V \ (/) ) )
43 dif0
 |-  ( _V \ (/) ) = _V
44 42 43 eqtrdi
 |-  ( (/) e. A -> ( _V \ |^| A ) = _V )
45 44 uneq2d
 |-  ( (/) e. A -> ( |^| B u. ( _V \ |^| A ) ) = ( |^| B u. _V ) )
46 unv
 |-  ( |^| B u. _V ) = _V
47 45 34 46 3eqtr3g
 |-  ( (/) e. A -> ( ( _V \ |^| A ) u. |^| B ) = _V )
48 47 adantl
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( ( _V \ |^| A ) u. |^| B ) = _V )
49 48 ineq2d
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i _V ) )
50 inv1
 |-  ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i _V ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B )
51 49 50 eqtr2di
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )
52 40 51 eqtrd
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )
53 39 52 oe0lem
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )