MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omopthlem2 Structured version   Visualization version   GIF version

Theorem omopthlem2 8661
Description: Lemma for omopthi 8662. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
Hypotheses
Ref Expression
omopthlem2.1 ๐ด โˆˆ ฯ‰
omopthlem2.2 ๐ต โˆˆ ฯ‰
omopthlem2.3 ๐ถ โˆˆ ฯ‰
omopthlem2.4 ๐ท โˆˆ ฯ‰
Assertion
Ref Expression
omopthlem2 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ ยฌ ((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต))

Proof of Theorem omopthlem2
StepHypRef Expression
1 omopthlem2.3 . . . . . . 7 ๐ถ โˆˆ ฯ‰
21, 1nnmcli 8617 . . . . . 6 (๐ถ ยทo ๐ถ) โˆˆ ฯ‰
3 omopthlem2.4 . . . . . 6 ๐ท โˆˆ ฯ‰
42, 3nnacli 8616 . . . . 5 ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ฯ‰
54nnoni 7864 . . . 4 ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ On
65onirri 6477 . . 3 ยฌ ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท)
7 eleq1 2821 . . 3 (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ†’ (((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท) โ†” (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท)))
86, 7mtbii 325 . 2 (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ†’ ยฌ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท))
9 nnaword1 8631 . . . 4 (((๐ถ ยทo ๐ถ) โˆˆ ฯ‰ โˆง ๐ท โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐ถ) โŠ† ((๐ถ ยทo ๐ถ) +o ๐ท))
102, 3, 9mp2an 690 . . 3 (๐ถ ยทo ๐ถ) โŠ† ((๐ถ ยทo ๐ถ) +o ๐ท)
11 omopthlem2.2 . . . . . . . . 9 ๐ต โˆˆ ฯ‰
12 omopthlem2.1 . . . . . . . . . . 11 ๐ด โˆˆ ฯ‰
1312, 11nnacli 8616 . . . . . . . . . 10 (๐ด +o ๐ต) โˆˆ ฯ‰
1413, 12nnacli 8616 . . . . . . . . 9 ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰
15 nnaword1 8631 . . . . . . . . 9 ((๐ต โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰) โ†’ ๐ต โŠ† (๐ต +o ((๐ด +o ๐ต) +o ๐ด)))
1611, 14, 15mp2an 690 . . . . . . . 8 ๐ต โŠ† (๐ต +o ((๐ด +o ๐ต) +o ๐ด))
17 nnacom 8619 . . . . . . . . 9 ((๐ต โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰) โ†’ (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต))
1811, 14, 17mp2an 690 . . . . . . . 8 (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต)
1916, 18sseqtri 4018 . . . . . . 7 ๐ต โŠ† (((๐ด +o ๐ต) +o ๐ด) +o ๐ต)
20 nnaass 8624 . . . . . . . . 9 (((๐ด +o ๐ต) โˆˆ ฯ‰ โˆง ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต)))
2113, 12, 11, 20mp3an 1461 . . . . . . . 8 (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต))
22 nnm2 8654 . . . . . . . . 9 ((๐ด +o ๐ต) โˆˆ ฯ‰ โ†’ ((๐ด +o ๐ต) ยทo 2o) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต)))
2313, 22ax-mp 5 . . . . . . . 8 ((๐ด +o ๐ต) ยทo 2o) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต))
2421, 23eqtr4i 2763 . . . . . . 7 (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) ยทo 2o)
2519, 24sseqtri 4018 . . . . . 6 ๐ต โŠ† ((๐ด +o ๐ต) ยทo 2o)
26 2onn 8643 . . . . . . . 8 2o โˆˆ ฯ‰
2713, 26nnmcli 8617 . . . . . . 7 ((๐ด +o ๐ต) ยทo 2o) โˆˆ ฯ‰
2813, 13nnmcli 8617 . . . . . . 7 ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰
29 nnawordi 8623 . . . . . . 7 ((๐ต โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) ยทo 2o) โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰) โ†’ (๐ต โŠ† ((๐ด +o ๐ต) ยทo 2o) โ†’ (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) โŠ† (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))))
3011, 27, 28, 29mp3an 1461 . . . . . 6 (๐ต โŠ† ((๐ด +o ๐ต) ยทo 2o) โ†’ (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) โŠ† (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))
3125, 30ax-mp 5 . . . . 5 (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) โŠ† (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))
32 nnacom 8619 . . . . . 6 ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))
3328, 11, 32mp2an 690 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))
34 nnacom 8619 . . . . . 6 ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) ยทo 2o) โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) = (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))
3528, 27, 34mp2an 690 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) = (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))
3631, 33, 353sstr4i 4025 . . . 4 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โŠ† (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o))
3713, 1omopthlem1 8660 . . . 4 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โˆˆ (๐ถ ยทo ๐ถ))
3828, 11nnacli 8616 . . . . . 6 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ฯ‰
3938nnoni 7864 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ On
402nnoni 7864 . . . . 5 (๐ถ ยทo ๐ถ) โˆˆ On
41 ontr2 6411 . . . . 5 (((((๐ด +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 ๐ถ)))
4239, 40, 41mp2an 690 . . . 4 (((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โŠ† (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โˆง (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โˆˆ (๐ถ ยทo ๐ถ)) โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ (๐ถ ยทo ๐ถ))
4336, 37, 42sylancr 587 . . 3 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ (๐ถ ยทo ๐ถ))
4410, 43sselid 3980 . 2 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท))
458, 44nsyl3 138 1 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ ยฌ ((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106   โŠ† wss 3948  Oncon0 6364  (class class class)co 7411  ฯ‰com 7857  2oc2o 8462   +o coa 8465   ยทo comu 8466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473
This theorem is referenced by:  omopthi  8662
  Copyright terms: Public domain W3C validator