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