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

Theorem wess 4805
Description: Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.)
Assertion
Ref Expression
wess  |-  ( A 
C_  B  ->  ( R  We  B  ->  R  We  A ) )

Proof of Theorem wess
StepHypRef Expression
1 frss 4785 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4757 . . 3  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
31, 2anim12d 563 . 2  |-  ( A 
C_  B  ->  (
( R  Fr  B  /\  R  Or  B
)  ->  ( R  Fr  A  /\  R  Or  A ) ) )
4 df-we 4779 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4779 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
63, 4, 53imtr4g 270 1  |-  ( A 
C_  B  ->  ( R  We  B  ->  R  We  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3426    Or wor 4738    Fr wfr 4774    We wwe 4776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-in 3433  df-ss 3440  df-po 4739  df-so 4740  df-fr 4777  df-we 4779
This theorem is referenced by:  wefrc  4812  trssord  4834  ordelord  4839  fnwelem  6787  ordtypelem8  7840  oismo  7855  cantnfcl  7976  cantnfclOLD  8006  infxpenlem  8281  ac10ct  8305  dfac12lem2  8414  cflim2  8533  cofsmo  8539  hsmexlem1  8696  smobeth  8851  canthwelem  8918  gruina  9086  ltwefz  11887  omsinds  27814  wfrlem5  27862  welb  28768  dnwech  29539  aomclem4  29548  dfac11  29553  onfrALTlem3  31552  onfrALTlem3VD  31923
  Copyright terms: Public domain W3C validator