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 ) ) )