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

Theorem wess 5011
Description: Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.)
Assertion
Ref Expression
wess (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))

Proof of Theorem wess
StepHypRef Expression
1 frss 4991 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 4963 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 583 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 4985 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 4985 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 283 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3535   Or wor 4944   Fr wfr 4980   We wwe 4982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-ral 2896  df-in 3542  df-ss 3549  df-po 4945  df-so 4946  df-fr 4983  df-we 4985
This theorem is referenced by:  wefrc  5018  trssord  5639  ordelord  5644  omsinds  6949  fnwelem  7152  wfrlem5  7279  dfrecs3  7329  ordtypelem8  8286  oismo  8301  cantnfcl  8420  infxpenlem  8692  ac10ct  8713  dfac12lem2  8822  cflim2  8941  cofsmo  8947  hsmexlem1  9104  smobeth  9260  canthwelem  9324  gruina  9492  ltwefz  12575  welb  32500  dnwech  36435  aomclem4  36444  dfac11  36449  onfrALTlem3  37579  onfrALTlem3VD  37944
  Copyright terms: Public domain W3C validator