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 ⊢ 𝐴 ∈ ω
omopthlem1.2 ⊢ 𝐶 ∈ ω
Assertion omopthlem1 ( 𝐴 ∈ 𝐶 → ( ( 𝐴 ·o 𝐴 ) +o ( 𝐴 ·o 2o ) ) ∈ ( 𝐶 ·o 𝐶 ) )

Proof

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