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

Theorem wess 5535
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 5515 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5486 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 608 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5509 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5509 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 297 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3933   Or wor 5466   Fr wfr 5504   We wwe 5506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ral 3140  df-in 3940  df-ss 3949  df-po 5467  df-so 5468  df-fr 5507  df-we 5509
This theorem is referenced by:  wefrc  5542  trssord  6201  ordelord  6206  omsinds  7589  fnwelem  7814  wfrlem5  7948  dfrecs3  7998  ordtypelem8  8977  oismo  8992  cantnfcl  9118  infxpenlem  9427  ac10ct  9448  dfac12lem2  9558  cflim2  9673  cofsmo  9679  hsmexlem1  9836  smobeth  9996  canthwelem  10060  gruina  10228  ltwefz  13319  dford5  32854  welb  34892  dnwech  39526  aomclem4  39535  dfac11  39540  onfrALTlem3  40755  onfrALTlem3VD  41098
  Copyright terms: Public domain W3C validator