This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omopthlem1

Description: Lemma for omopthi . (Contributed by Scott Fenton, 18-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses omopthlem1.1 
|- A e. _om
omopthlem1.2 
|- C e. _om
Assertion omopthlem1 
|- ( A e. C -> ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) )

Proof

Step Hyp Ref Expression
1 omopthlem1.1 
 |-  A e. _om
2 omopthlem1.2 
 |-  C e. _om
3 peano2 
 |-  ( A e. _om -> suc A e. _om )
4 1 3 ax-mp 
 |-  suc A e. _om
5 nnmwordi 
 |-  ( ( suc A e. _om /\ C e. _om /\ suc A e. _om ) -> ( suc A C_ C -> ( suc A .o suc A ) C_ ( suc A .o C ) ) )
6 4 2 4 5 mp3an 
 |-  ( suc A C_ C -> ( suc A .o suc A ) C_ ( suc A .o C ) )
7 nnmwordri 
 |-  ( ( suc A e. _om /\ C e. _om /\ C e. _om ) -> ( suc A C_ C -> ( suc A .o C ) C_ ( C .o C ) ) )
8 4 2 2 7 mp3an 
 |-  ( suc A C_ C -> ( suc A .o C ) C_ ( C .o C ) )
9 6 8 sstrd 
 |-  ( suc A C_ C -> ( suc A .o suc A ) C_ ( C .o C ) )
10 1 nnoni 
 |-  A e. On
11 2 nnoni 
 |-  C e. On
12 10 11 onsucssi 
 |-  ( A e. C <-> suc A C_ C )
13 1 1 nnmcli 
 |-  ( A .o A ) e. _om
14 2onn 
 |-  2o e. _om
15 1 14 nnmcli 
 |-  ( A .o 2o ) e. _om
16 13 15 nnacli 
 |-  ( ( A .o A ) +o ( A .o 2o ) ) e. _om
17 16 nnoni 
 |-  ( ( A .o A ) +o ( A .o 2o ) ) e. On
18 2 2 nnmcli 
 |-  ( C .o C ) e. _om
19 18 nnoni 
 |-  ( C .o C ) e. On
20 17 19 onsucssi 
 |-  ( ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) <-> suc ( ( A .o A ) +o ( A .o 2o ) ) C_ ( C .o C ) )
21 4 1 nnmcli 
 |-  ( suc A .o A ) e. _om
22 nnasuc 
 |-  ( ( ( suc A .o A ) e. _om /\ A e. _om ) -> ( ( suc A .o A ) +o suc A ) = suc ( ( suc A .o A ) +o A ) )
23 21 1 22 mp2an 
 |-  ( ( suc A .o A ) +o suc A ) = suc ( ( suc A .o A ) +o A )
24 nnmsuc 
 |-  ( ( suc A e. _om /\ A e. _om ) -> ( suc A .o suc A ) = ( ( suc A .o A ) +o suc A ) )
25 4 1 24 mp2an 
 |-  ( suc A .o suc A ) = ( ( suc A .o A ) +o suc A )
26 nnaass 
 |-  ( ( ( A .o A ) e. _om /\ A e. _om /\ A e. _om ) -> ( ( ( A .o A ) +o A ) +o A ) = ( ( A .o A ) +o ( A +o A ) ) )
27 13 1 1 26 mp3an 
 |-  ( ( ( A .o A ) +o A ) +o A ) = ( ( A .o A ) +o ( A +o A ) )
28 nnmcom 
 |-  ( ( suc A e. _om /\ A e. _om ) -> ( suc A .o A ) = ( A .o suc A ) )
29 4 1 28 mp2an 
 |-  ( suc A .o A ) = ( A .o suc A )
30 nnmsuc 
 |-  ( ( A e. _om /\ A e. _om ) -> ( A .o suc A ) = ( ( A .o A ) +o A ) )
31 1 1 30 mp2an 
 |-  ( A .o suc A ) = ( ( A .o A ) +o A )
32 29 31 eqtri 
 |-  ( suc A .o A ) = ( ( A .o A ) +o A )
33 32 oveq1i 
 |-  ( ( suc A .o A ) +o A ) = ( ( ( A .o A ) +o A ) +o A )
34 nnm2 
 |-  ( A e. _om -> ( A .o 2o ) = ( A +o A ) )
35 1 34 ax-mp 
 |-  ( A .o 2o ) = ( A +o A )
36 35 oveq2i 
 |-  ( ( A .o A ) +o ( A .o 2o ) ) = ( ( A .o A ) +o ( A +o A ) )
37 27 33 36 3eqtr4ri 
 |-  ( ( A .o A ) +o ( A .o 2o ) ) = ( ( suc A .o A ) +o A )
38 suceq 
 |-  ( ( ( A .o A ) +o ( A .o 2o ) ) = ( ( suc A .o A ) +o A ) -> suc ( ( A .o A ) +o ( A .o 2o ) ) = suc ( ( suc A .o A ) +o A ) )
39 37 38 ax-mp 
 |-  suc ( ( A .o A ) +o ( A .o 2o ) ) = suc ( ( suc A .o A ) +o A )
40 23 25 39 3eqtr4ri 
 |-  suc ( ( A .o A ) +o ( A .o 2o ) ) = ( suc A .o suc A )
41 40 sseq1i 
 |-  ( suc ( ( A .o A ) +o ( A .o 2o ) ) C_ ( C .o C ) <-> ( suc A .o suc A ) C_ ( C .o C ) )
42 20 41 bitri 
 |-  ( ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) <-> ( suc A .o suc A ) C_ ( C .o C ) )
43 9 12 42 3imtr4i 
 |-  ( A e. C -> ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) )