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

Theorem omopthlem2 8659
Description: Lemma for omopthi 8660. (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 8615 . . . . . 6 (๐ถ ยทo ๐ถ) โˆˆ ฯ‰
3 omopthlem2.4 . . . . . 6 ๐ท โˆˆ ฯ‰
42, 3nnacli 8614 . . . . 5 ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ฯ‰
54nnoni 7862 . . . 4 ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ On
65onirri 6478 . . 3 ยฌ ((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท)
7 eleq1 2822 . . 3 (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ†’ (((๐ถ ยทo ๐ถ) +o ๐ท) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท) โ†” (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท)))
86, 7mtbii 326 . 2 (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ†’ ยฌ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ((๐ถ ยทo ๐ถ) +o ๐ท))
9 nnaword1 8629 . . . 4 (((๐ถ ยทo ๐ถ) โˆˆ ฯ‰ โˆง ๐ท โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐ถ) โŠ† ((๐ถ ยทo ๐ถ) +o ๐ท))
102, 3, 9mp2an 691 . . 3 (๐ถ ยทo ๐ถ) โŠ† ((๐ถ ยทo ๐ถ) +o ๐ท)
11 omopthlem2.2 . . . . . . . . 9 ๐ต โˆˆ ฯ‰
12 omopthlem2.1 . . . . . . . . . . 11 ๐ด โˆˆ ฯ‰
1312, 11nnacli 8614 . . . . . . . . . 10 (๐ด +o ๐ต) โˆˆ ฯ‰
1413, 12nnacli 8614 . . . . . . . . 9 ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰
15 nnaword1 8629 . . . . . . . . 9 ((๐ต โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰) โ†’ ๐ต โŠ† (๐ต +o ((๐ด +o ๐ต) +o ๐ด)))
1611, 14, 15mp2an 691 . . . . . . . 8 ๐ต โŠ† (๐ต +o ((๐ด +o ๐ต) +o ๐ด))
17 nnacom 8617 . . . . . . . . 9 ((๐ต โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) +o ๐ด) โˆˆ ฯ‰) โ†’ (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต))
1811, 14, 17mp2an 691 . . . . . . . 8 (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต)
1916, 18sseqtri 4019 . . . . . . 7 ๐ต โŠ† (((๐ด +o ๐ต) +o ๐ด) +o ๐ต)
20 nnaass 8622 . . . . . . . . 9 (((๐ด +o ๐ต) โˆˆ ฯ‰ โˆง ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต)))
2113, 12, 11, 20mp3an 1462 . . . . . . . 8 (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต))
22 nnm2 8652 . . . . . . . . 9 ((๐ด +o ๐ต) โˆˆ ฯ‰ โ†’ ((๐ด +o ๐ต) ยทo 2o) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต)))
2313, 22ax-mp 5 . . . . . . . 8 ((๐ด +o ๐ต) ยทo 2o) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต))
2421, 23eqtr4i 2764 . . . . . . 7 (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) ยทo 2o)
2519, 24sseqtri 4019 . . . . . 6 ๐ต โŠ† ((๐ด +o ๐ต) ยทo 2o)
26 2onn 8641 . . . . . . . 8 2o โˆˆ ฯ‰
2713, 26nnmcli 8615 . . . . . . 7 ((๐ด +o ๐ต) ยทo 2o) โˆˆ ฯ‰
2813, 13nnmcli 8615 . . . . . . 7 ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰
29 nnawordi 8621 . . . . . . 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 1462 . . . . . 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 8617 . . . . . 6 ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))
3328, 11, 32mp2an 691 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))
34 nnacom 8617 . . . . . 6 ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โˆˆ ฯ‰ โˆง ((๐ด +o ๐ต) ยทo 2o) โˆˆ ฯ‰) โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) = (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))
3528, 27, 34mp2an 691 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) = (((๐ด +o ๐ต) ยทo 2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))
3631, 33, 353sstr4i 4026 . . . 4 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โŠ† (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o))
3713, 1omopthlem1 8658 . . . 4 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โˆˆ (๐ถ ยทo ๐ถ))
3828, 11nnacli 8614 . . . . . 6 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ ฯ‰
3938nnoni 7862 . . . . 5 (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ On
402nnoni 7862 . . . . 5 (๐ถ ยทo ๐ถ) โˆˆ On
41 ontr2 6412 . . . . 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 691 . . . 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 588 . . 3 ((๐ด +o ๐ต) โˆˆ ๐ถ โ†’ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โˆˆ (๐ถ ยทo ๐ถ))
4410, 43sselid 3981 . 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 397   = wceq 1542   โˆˆ wcel 2107   โŠ† wss 3949  Oncon0 6365  (class class class)co 7409  ฯ‰com 7855  2oc2o 8460   +o coa 8463   ยทo comu 8464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471
This theorem is referenced by:  omopthi  8660
  Copyright terms: Public domain W3C validator