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∈ω
omopthlem1.2 ⊢C∈ω
Assertion omopthlem1 ⊢A∈C→A⋅𝑜A+𝑜A⋅𝑜2𝑜∈C⋅𝑜C

Proof

Step Hyp Ref Expression
1 omopthlem1.1 ⊢A∈ω
2 omopthlem1.2 ⊢C∈ω
3 peano2 ⊢A∈ω→suc⁡A∈ω
4 1 3 ax-mp ⊢suc⁡A∈ω
5 nnmwordi ⊢suc⁡A∈ω∧C∈ω∧suc⁡A∈ω→suc⁡A⊆C→suc⁡A⋅𝑜suc⁡A⊆suc⁡A⋅𝑜C
6 4 2 4 5 mp3an ⊢suc⁡A⊆C→suc⁡A⋅𝑜suc⁡A⊆suc⁡A⋅𝑜C
7 nnmwordri ⊢suc⁡A∈ω∧C∈ω∧C∈ω→suc⁡A⊆C→suc⁡A⋅𝑜C⊆C⋅𝑜C
8 4 2 2 7 mp3an ⊢suc⁡A⊆C→suc⁡A⋅𝑜C⊆C⋅𝑜C
9 6 8 sstrd ⊢suc⁡A⊆C→suc⁡A⋅𝑜suc⁡A⊆C⋅𝑜C
10 1 nnoni ⊢A∈On
11 2 nnoni ⊢C∈On
12 10 11 onsucssi ⊢A∈C↔suc⁡A⊆C
13 1 1 nnmcli ⊢A⋅𝑜A∈ω
14 2onn ⊢2𝑜∈ω
15 1 14 nnmcli ⊢A⋅𝑜2𝑜∈ω
16 13 15 nnacli ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜∈ω
17 16 nnoni ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜∈On
18 2 2 nnmcli ⊢C⋅𝑜C∈ω
19 18 nnoni ⊢C⋅𝑜C∈On
20 17 19 onsucssi ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜∈C⋅𝑜C↔suc⁡A⋅𝑜A+𝑜A⋅𝑜2𝑜⊆C⋅𝑜C
21 4 1 nnmcli ⊢suc⁡A⋅𝑜A∈ω
22 nnasuc ⊢suc⁡A⋅𝑜A∈ω∧A∈ω→suc⁡A⋅𝑜A+𝑜suc⁡A=suc⁡suc⁡A⋅𝑜A+𝑜A
23 21 1 22 mp2an ⊢suc⁡A⋅𝑜A+𝑜suc⁡A=suc⁡suc⁡A⋅𝑜A+𝑜A
24 nnmsuc ⊢suc⁡A∈ω∧A∈ω→suc⁡A⋅𝑜suc⁡A=suc⁡A⋅𝑜A+𝑜suc⁡A
25 4 1 24 mp2an ⊢suc⁡A⋅𝑜suc⁡A=suc⁡A⋅𝑜A+𝑜suc⁡A
26 nnaass ⊢A⋅𝑜A∈ω∧A∈ω∧A∈ω→A⋅𝑜A+𝑜A+𝑜A=A⋅𝑜A+𝑜A+𝑜A
27 13 1 1 26 mp3an ⊢A⋅𝑜A+𝑜A+𝑜A=A⋅𝑜A+𝑜A+𝑜A
28 nnmcom ⊢suc⁡A∈ω∧A∈ω→suc⁡A⋅𝑜A=A⋅𝑜suc⁡A
29 4 1 28 mp2an ⊢suc⁡A⋅𝑜A=A⋅𝑜suc⁡A
30 nnmsuc ⊢A∈ω∧A∈ω→A⋅𝑜suc⁡A=A⋅𝑜A+𝑜A
31 1 1 30 mp2an ⊢A⋅𝑜suc⁡A=A⋅𝑜A+𝑜A
32 29 31 eqtri ⊢suc⁡A⋅𝑜A=A⋅𝑜A+𝑜A
33 32 oveq1i ⊢suc⁡A⋅𝑜A+𝑜A=A⋅𝑜A+𝑜A+𝑜A
34 nnm2 ⊢A∈ω→A⋅𝑜2𝑜=A+𝑜A
35 1 34 ax-mp ⊢A⋅𝑜2𝑜=A+𝑜A
36 35 oveq2i ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜=A⋅𝑜A+𝑜A+𝑜A
37 27 33 36 3eqtr4ri ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜=suc⁡A⋅𝑜A+𝑜A
38 suceq ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜=suc⁡A⋅𝑜A+𝑜A→suc⁡A⋅𝑜A+𝑜A⋅𝑜2𝑜=suc⁡suc⁡A⋅𝑜A+𝑜A
39 37 38 ax-mp ⊢suc⁡A⋅𝑜A+𝑜A⋅𝑜2𝑜=suc⁡suc⁡A⋅𝑜A+𝑜A
40 23 25 39 3eqtr4ri ⊢suc⁡A⋅𝑜A+𝑜A⋅𝑜2𝑜=suc⁡A⋅𝑜suc⁡A
41 40 sseq1i ⊢suc⁡A⋅𝑜A+𝑜A⋅𝑜2𝑜⊆C⋅𝑜C↔suc⁡A⋅𝑜suc⁡A⊆C⋅𝑜C
42 20 41 bitri ⊢A⋅𝑜A+𝑜A⋅𝑜2𝑜∈C⋅𝑜C↔suc⁡A⋅𝑜suc⁡A⊆C⋅𝑜C
43 9 12 42 3imtr4i ⊢A∈C→A⋅𝑜A+𝑜A⋅𝑜2𝑜∈C⋅𝑜C