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