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

Theorem wess 4396
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 4376 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4348 . . 3  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
31, 2anim12d 546 . 2  |-  ( A 
C_  B  ->  (
( R  Fr  B  /\  R  Or  B
)  ->  ( R  Fr  A  /\  R  Or  A ) ) )
4 df-we 4370 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4370 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
63, 4, 53imtr4g 261 1  |-  ( A 
C_  B  ->  ( R  We  B  ->  R  We  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3165    Or wor 4329    Fr wfr 4365    We wwe 4367
This theorem is referenced by:  wefrc  4403  trssord  4425  ordelord  4430  fnwelem  6246  ordtypelem8  7256  oismo  7271  cantnfcl  7384  infxpenlem  7657  ac10ct  7677  dfac12lem2  7786  cflim2  7905  cofsmo  7911  hsmexlem1  8068  smobeth  8224  canthwelem  8288  gruina  8456  ltwefz  11042  omsinds  24290  wfrlem5  24331  tfrALTlem  24347  welb  26520  dnwech  27248  aomclem4  27257  dfac11  27263  onfrALTlem3  28608  onfrALTlem3VD  28979
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-in 3172  df-ss 3179  df-po 4330  df-so 4331  df-fr 4368  df-we 4370
  Copyright terms: Public domain W3C validator