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 A ω
omopthlem2.2 B ω
omopthlem2.3 C ω
omopthlem2.4 D ω
Assertion omopthlem2 A + 𝑜 B C ¬ C 𝑜 C + 𝑜 D = A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B

Proof

Step Hyp Ref Expression
1 omopthlem2.1 A ω
2 omopthlem2.2 B ω
3 omopthlem2.3 C ω
4 omopthlem2.4 D ω
5 3 3 nnmcli C 𝑜 C ω
6 5 4 nnacli C 𝑜 C + 𝑜 D ω
7 6 nnoni C 𝑜 C + 𝑜 D On
8 7 onirri ¬ C 𝑜 C + 𝑜 D C 𝑜 C + 𝑜 D
9 eleq1 C 𝑜 C + 𝑜 D = A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C + 𝑜 D C 𝑜 C + 𝑜 D A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C + 𝑜 D
10 8 9 mtbii C 𝑜 C + 𝑜 D = A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B ¬ A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C + 𝑜 D
11 nnaword1 C 𝑜 C ω D ω C 𝑜 C C 𝑜 C + 𝑜 D
12 5 4 11 mp2an C 𝑜 C C 𝑜 C + 𝑜 D
13 1 2 nnacli A + 𝑜 B ω
14 13 1 nnacli A + 𝑜 B + 𝑜 A ω
15 nnaword1 B ω A + 𝑜 B + 𝑜 A ω B B + 𝑜 A + 𝑜 B + 𝑜 A
16 2 14 15 mp2an B B + 𝑜 A + 𝑜 B + 𝑜 A
17 nnacom B ω A + 𝑜 B + 𝑜 A ω B + 𝑜 A + 𝑜 B + 𝑜 A = A + 𝑜 B + 𝑜 A + 𝑜 B
18 2 14 17 mp2an B + 𝑜 A + 𝑜 B + 𝑜 A = A + 𝑜 B + 𝑜 A + 𝑜 B
19 16 18 sseqtri B A + 𝑜 B + 𝑜 A + 𝑜 B
20 nnaass A + 𝑜 B ω A ω B ω A + 𝑜 B + 𝑜 A + 𝑜 B = A + 𝑜 B + 𝑜 A + 𝑜 B
21 13 1 2 20 mp3an A + 𝑜 B + 𝑜 A + 𝑜 B = A + 𝑜 B + 𝑜 A + 𝑜 B
22 nnm2 A + 𝑜 B ω A + 𝑜 B 𝑜 2 𝑜 = A + 𝑜 B + 𝑜 A + 𝑜 B
23 13 22 ax-mp A + 𝑜 B 𝑜 2 𝑜 = A + 𝑜 B + 𝑜 A + 𝑜 B
24 21 23 eqtr4i A + 𝑜 B + 𝑜 A + 𝑜 B = A + 𝑜 B 𝑜 2 𝑜
25 19 24 sseqtri B A + 𝑜 B 𝑜 2 𝑜
26 2onn 2 𝑜 ω
27 13 26 nnmcli A + 𝑜 B 𝑜 2 𝑜 ω
28 13 13 nnmcli A + 𝑜 B 𝑜 A + 𝑜 B ω
29 nnawordi B ω A + 𝑜 B 𝑜 2 𝑜 ω A + 𝑜 B 𝑜 A + 𝑜 B ω B A + 𝑜 B 𝑜 2 𝑜 B + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B A + 𝑜 B 𝑜 2 𝑜 + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
30 2 27 28 29 mp3an B A + 𝑜 B 𝑜 2 𝑜 B + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B A + 𝑜 B 𝑜 2 𝑜 + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
31 25 30 ax-mp B + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B A + 𝑜 B 𝑜 2 𝑜 + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
32 nnacom A + 𝑜 B 𝑜 A + 𝑜 B ω B ω A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B = B + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
33 28 2 32 mp2an A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B = B + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
34 nnacom A + 𝑜 B 𝑜 A + 𝑜 B ω A + 𝑜 B 𝑜 2 𝑜 ω A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 = A + 𝑜 B 𝑜 2 𝑜 + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
35 28 27 34 mp2an A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 = A + 𝑜 B 𝑜 2 𝑜 + 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B
36 31 33 35 3sstr4i A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜
37 13 3 omopthlem1 A + 𝑜 B C A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 C 𝑜 C
38 28 2 nnacli A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B ω
39 38 nnoni A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B On
40 5 nnoni C 𝑜 C On
41 ontr2 A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B On C 𝑜 C On A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 C 𝑜 C A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C
42 39 40 41 mp2an A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 A + 𝑜 B 𝑜 2 𝑜 C 𝑜 C A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C
43 36 37 42 sylancr A + 𝑜 B C A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C
44 12 43 sselid A + 𝑜 B C A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B C 𝑜 C + 𝑜 D
45 10 44 nsyl3 A + 𝑜 B C ¬ C 𝑜 C + 𝑜 D = A + 𝑜 B 𝑜 A + 𝑜 B + 𝑜 B