Metamath Proof Explorer

Theorem oesuclem

Description: Lemma for oesuc . (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypotheses oesuclem.1 
|- Lim X
oesuclem.2 
|- ( B e. X -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
Assertion oesuclem 
|- ( ( A e. On /\ B e. X ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )

Proof

Step Hyp Ref Expression
1 oesuclem.1 
 |-  Lim X
2 oesuclem.2 
 |-  ( B e. X -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
3 oveq1 
 |-  ( A = (/) -> ( A ^o suc B ) = ( (/) ^o suc B ) )
4 limord 
 |-  ( Lim X -> Ord X )
5 1 4 ax-mp 
 |-  Ord X
6 ordelord 
 |-  ( ( Ord X /\ B e. X ) -> Ord B )
7 5 6 mpan 
 |-  ( B e. X -> Ord B )
8 0elsuc 
 |-  ( Ord B -> (/) e. suc B )
9 7 8 syl 
 |-  ( B e. X -> (/) e. suc B )
10 limsuc 
 |-  ( Lim X -> ( B e. X <-> suc B e. X ) )
11 1 10 ax-mp 
 |-  ( B e. X <-> suc B e. X )
12 ordelon 
 |-  ( ( Ord X /\ suc B e. X ) -> suc B e. On )
13 5 12 mpan 
 |-  ( suc B e. X -> suc B e. On )
14 oe0m1 
 |-  ( suc B e. On -> ( (/) e. suc B <-> ( (/) ^o suc B ) = (/) ) )
15 13 14 syl 
 |-  ( suc B e. X -> ( (/) e. suc B <-> ( (/) ^o suc B ) = (/) ) )
16 11 15 sylbi 
 |-  ( B e. X -> ( (/) e. suc B <-> ( (/) ^o suc B ) = (/) ) )
17 9 16 mpbid 
 |-  ( B e. X -> ( (/) ^o suc B ) = (/) )
18 3 17 sylan9eqr 
 |-  ( ( B e. X /\ A = (/) ) -> ( A ^o suc B ) = (/) )
19 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
20 id 
 |-  ( A = (/) -> A = (/) )
21 19 20 oveq12d 
 |-  ( A = (/) -> ( ( A ^o B ) .o A ) = ( ( (/) ^o B ) .o (/) ) )
22 ordelon 
 |-  ( ( Ord X /\ B e. X ) -> B e. On )
23 5 22 mpan 
 |-  ( B e. X -> B e. On )
24 oveq2 
 |-  ( B = (/) -> ( (/) ^o B ) = ( (/) ^o (/) ) )
25 oe0m0 
 |-  ( (/) ^o (/) ) = 1o
26 1on 
 |-  1o e. On
27 25 26 eqeltri 
 |-  ( (/) ^o (/) ) e. On
28 24 27 eqeltrdi 
 |-  ( B = (/) -> ( (/) ^o B ) e. On )
29 28 adantl 
 |-  ( ( B e. X /\ B = (/) ) -> ( (/) ^o B ) e. On )
30 oe0m1 
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
31 23 30 syl 
 |-  ( B e. X -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
32 31 biimpa 
 |-  ( ( B e. X /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
33 0elon 
 |-  (/) e. On
34 32 33 eqeltrdi 
 |-  ( ( B e. X /\ (/) e. B ) -> ( (/) ^o B ) e. On )
35 34 adantll 
 |-  ( ( ( B e. On /\ B e. X ) /\ (/) e. B ) -> ( (/) ^o B ) e. On )
36 29 35 oe0lem 
 |-  ( ( B e. On /\ B e. X ) -> ( (/) ^o B ) e. On )
37 23 36 mpancom 
 |-  ( B e. X -> ( (/) ^o B ) e. On )
38 om0 
 |-  ( ( (/) ^o B ) e. On -> ( ( (/) ^o B ) .o (/) ) = (/) )
39 37 38 syl 
 |-  ( B e. X -> ( ( (/) ^o B ) .o (/) ) = (/) )
40 21 39 sylan9eqr 
 |-  ( ( B e. X /\ A = (/) ) -> ( ( A ^o B ) .o A ) = (/) )
41 18 40 eqtr4d 
 |-  ( ( B e. X /\ A = (/) ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
42 2 ad2antlr 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
43 11 13 sylbi 
 |-  ( B e. X -> suc B e. On )
44 oevn0 
 |-  ( ( ( A e. On /\ suc B e. On ) /\ (/) e. A ) -> ( A ^o suc B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) )
45 43 44 sylanl2 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( A ^o suc B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) )
46 ovex 
 |-  ( A ^o B ) e. _V
47 oveq1 
 |-  ( x = ( A ^o B ) -> ( x .o A ) = ( ( A ^o B ) .o A ) )
48 eqid 
 |-  ( x e. _V |-> ( x .o A ) ) = ( x e. _V |-> ( x .o A ) )
49 ovex 
 |-  ( ( A ^o B ) .o A ) e. _V
50 47 48 49 fvmpt 
 |-  ( ( A ^o B ) e. _V -> ( ( x e. _V |-> ( x .o A ) ) ` ( A ^o B ) ) = ( ( A ^o B ) .o A ) )
51 46 50 ax-mp 
 |-  ( ( x e. _V |-> ( x .o A ) ) ` ( A ^o B ) ) = ( ( A ^o B ) .o A )
52 oevn0 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
53 23 52 sylanl2 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
54 53 fveq2d 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( ( x e. _V |-> ( x .o A ) ) ` ( A ^o B ) ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
55 51 54 eqtr3id 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( ( A ^o B ) .o A ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
56 42 45 55 3eqtr4d 
 |-  ( ( ( A e. On /\ B e. X ) /\ (/) e. A ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
57 41 56 oe0lem 
 |-  ( ( A e. On /\ B e. X ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )