Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tosso Structured version   Unicode version

Theorem tosso 16220
 Description: Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015.)
Hypotheses
Ref Expression
tosso.b
tosso.l
tosso.s
Assertion
Ref Expression
tosso Toset

Proof of Theorem tosso
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tosso.b . . . . . . . . 9
2 tosso.l . . . . . . . . 9
3 tosso.s . . . . . . . . 9
41, 2, 3pleval2 16149 . . . . . . . 8
543expb 1206 . . . . . . 7
61, 2, 3pleval2 16149 . . . . . . . . . 10
7 equcom 1848 . . . . . . . . . . 11
87orbi2i 521 . . . . . . . . . 10
96, 8syl6bb 264 . . . . . . . . 9
1093com23 1211 . . . . . . . 8
11103expb 1206 . . . . . . 7
125, 11orbi12d 714 . . . . . 6
13 df-3or 983 . . . . . . 7
14 or32 529 . . . . . . . 8
15 orordir 533 . . . . . . . 8
1614, 15bitri 252 . . . . . . 7
1713, 16bitri 252 . . . . . 6
1812, 17syl6bbr 266 . . . . 5
19182ralbidva 2802 . . . 4
2019pm5.32i 641 . . 3
211, 2, 3pospo 16157 . . . 4
2221anbi1d 709 . . 3
2320, 22syl5bb 260 . 2
241, 2istos 16219 . 2 Toset
25 df-so 4713 . . . 4
2625anbi1i 699 . . 3
27 an32 805 . . 3
2826, 27bitri 252 . 2
2923, 24, 283bitr4g 291 1 Toset
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wo 369   wa 370   w3o 981   w3a 982   wceq 1437   wcel 1872  wral 2709   wss 3374   class class class wbr 4361   cid 4701   wpo 4710   wor 4711   cres 4793  cfv 5539  cbs 15059  cple 15135  cpo 16123  cplt 16124  Tosetctos 16217 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-res 4803  df-iota 5503  df-fun 5541  df-fv 5547  df-preset 16111  df-poset 16129  df-plt 16142  df-toset 16218 This theorem is referenced by:  opsrtoslem2  18646  opsrso  18648  retos  19123  toslub  28375  tosglb  28377  tosglbOLD  28378  orngsqr  28514
 Copyright terms: Public domain W3C validator