Metamath Proof Explorer

Theorem omopthlem2

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

Ref Expression
Hypotheses omopthlem2.1 ⊢ 𝐴 ∈ ω
omopthlem2.2 ⊢ 𝐵 ∈ ω
omopthlem2.3 ⊢ 𝐶 ∈ ω
omopthlem2.4 ⊢ 𝐷 ∈ ω
Assertion omopthlem2 ( ( 𝐴 +o 𝐵 ) ∈ 𝐶 → ¬ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 omopthlem2.1 ⊢ 𝐴 ∈ ω
2 omopthlem2.2 ⊢ 𝐵 ∈ ω
3 omopthlem2.3 ⊢ 𝐶 ∈ ω
4 omopthlem2.4 ⊢ 𝐷 ∈ ω
5 3 3 nnmcli ⊢ ( 𝐶 ·o 𝐶 ) ∈ ω
6 5 4 nnacli ⊢ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ∈ ω
7 6 nnoni ⊢ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ∈ On
8 7 onirri ⊢ ¬ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ∈ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 )
9 eleq1 ⊢ ( ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) → ( ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ∈ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ↔ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) ) )
10 8 9 mtbii ⊢ ( ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) → ¬ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) )
11 nnaword1 ⊢ ( ( ( 𝐶 ·o 𝐶 ) ∈ ω ∧ 𝐷 ∈ ω ) → ( 𝐶 ·o 𝐶 ) ⊆ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) )
12 5 4 11 mp2an ⊢ ( 𝐶 ·o 𝐶 ) ⊆ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 )
13 1 2 nnacli ⊢ ( 𝐴 +o 𝐵 ) ∈ ω
14 13 1 nnacli ⊢ ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ∈ ω
15 nnaword1 ⊢ ( ( 𝐵 ∈ ω ∧ ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ∈ ω ) → 𝐵 ⊆ ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ) )
16 2 14 15 mp2an ⊢ 𝐵 ⊆ ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) )
17 nnacom ⊢ ( ( 𝐵 ∈ ω ∧ ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ∈ ω ) → ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ) = ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 ) )
18 2 14 17 mp2an ⊢ ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) ) = ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 )
19 16 18 sseqtri ⊢ 𝐵 ⊆ ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 )
20 nnaass ⊢ ( ( ( 𝐴 +o 𝐵 ) ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 ) = ( ( 𝐴 +o 𝐵 ) +o ( 𝐴 +o 𝐵 ) ) )
21 13 1 2 20 mp3an ⊢ ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 ) = ( ( 𝐴 +o 𝐵 ) +o ( 𝐴 +o 𝐵 ) )
22 nnm2 ⊢ ( ( 𝐴 +o 𝐵 ) ∈ ω → ( ( 𝐴 +o 𝐵 ) ·o 2o ) = ( ( 𝐴 +o 𝐵 ) +o ( 𝐴 +o 𝐵 ) ) )
23 13 22 ax-mp ⊢ ( ( 𝐴 +o 𝐵 ) ·o 2o ) = ( ( 𝐴 +o 𝐵 ) +o ( 𝐴 +o 𝐵 ) )
24 21 23 eqtr4i ⊢ ( ( ( 𝐴 +o 𝐵 ) +o 𝐴 ) +o 𝐵 ) = ( ( 𝐴 +o 𝐵 ) ·o 2o )
25 19 24 sseqtri ⊢ 𝐵 ⊆ ( ( 𝐴 +o 𝐵 ) ·o 2o )
26 2onn ⊢ 2o ∈ ω
27 13 26 nnmcli ⊢ ( ( 𝐴 +o 𝐵 ) ·o 2o ) ∈ ω
28 13 13 nnmcli ⊢ ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω
29 nnawordi ⊢ ( ( 𝐵 ∈ ω ∧ ( ( 𝐴 +o 𝐵 ) ·o 2o ) ∈ ω ∧ ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω ) → ( 𝐵 ⊆ ( ( 𝐴 +o 𝐵 ) ·o 2o ) → ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o 2o ) +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) ) )
30 2 27 28 29 mp3an ⊢ ( 𝐵 ⊆ ( ( 𝐴 +o 𝐵 ) ·o 2o ) → ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o 2o ) +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) )
31 25 30 ax-mp ⊢ ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o 2o ) +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) )
32 nnacom ⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) )
33 28 2 32 mp2an ⊢ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( 𝐵 +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) )
34 nnacom ⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω ∧ ( ( 𝐴 +o 𝐵 ) ·o 2o ) ∈ ω ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) = ( ( ( 𝐴 +o 𝐵 ) ·o 2o ) +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ) )
35 28 27 34 mp2an ⊢ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) = ( ( ( 𝐴 +o 𝐵 ) ·o 2o ) +o ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) )
36 31 33 35 3sstr4i ⊢ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) )
37 13 3 omopthlem1 ⊢ ( ( 𝐴 +o 𝐵 ) ∈ 𝐶 → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) ∈ ( 𝐶 ·o 𝐶 ) )
38 28 2 nnacli ⊢ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ω
39 38 nnoni ⊢ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ On
40 5 nnoni ⊢ ( 𝐶 ·o 𝐶 ) ∈ On
41 ontr2 ⊢ ( ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ On ∧ ( 𝐶 ·o 𝐶 ) ∈ On ) → ( ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) ∧ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) ∈ ( 𝐶 ·o 𝐶 ) ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( 𝐶 ·o 𝐶 ) ) )
42 39 40 41 mp2an ⊢ ( ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ⊆ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) ∧ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o ( ( 𝐴 +o 𝐵 ) ·o 2o ) ) ∈ ( 𝐶 ·o 𝐶 ) ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( 𝐶 ·o 𝐶 ) )
43 36 37 42 sylancr ⊢ ( ( 𝐴 +o 𝐵 ) ∈ 𝐶 → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( 𝐶 ·o 𝐶 ) )
44 12 43 sseldi ⊢ ( ( 𝐴 +o 𝐵 ) ∈ 𝐶 → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ∈ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) )
45 10 44 nsyl3 ⊢ ( ( 𝐴 +o 𝐵 ) ∈ 𝐶 → ¬ ( ( 𝐶 ·o 𝐶 ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) )