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

Theorem wess 5664
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 5644 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5609 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 610 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5634 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5634 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wss 3949   Or wor 5588   Fr wfr 5629   We wwe 5631
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-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-po 5589  df-so 5590  df-fr 5632  df-we 5634
This theorem is referenced by:  wefrc  5671  trssord  6382  ordelord  6387  dford5  7771  omsinds  7876  omsindsOLD  7877  fnwelem  8117  wfrlem5OLD  8313  dfrecs3  8372  dfrecs3OLD  8373  ordtypelem8  9520  oismo  9535  cantnfcl  9662  infxpenlem  10008  ac10ct  10029  dfac12lem2  10139  cflim2  10258  cofsmo  10264  hsmexlem1  10421  smobeth  10581  canthwelem  10645  gruina  10813  ltwefz  13928  welb  36604  dnwech  41790  aomclem4  41799  dfac11  41804  oaun3lem1  42124  onfrALTlem3  43305  onfrALTlem3VD  43648
  Copyright terms: Public domain W3C validator