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

Theorem wess 4380
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 4360 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4332 . . 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 4354 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4354 . 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 3152    Or wor 4313    Fr wfr 4349    We wwe 4351
This theorem is referenced by:  wefrc  4387  trssord  4409  ordelord  4414  fnwelem  6230  ordtypelem8  7240  oismo  7255  cantnfcl  7368  infxpenlem  7641  ac10ct  7661  dfac12lem2  7770  cflim2  7889  cofsmo  7895  hsmexlem1  8052  smobeth  8208  canthwelem  8272  gruina  8440  ltwefz  11026  omsinds  24219  wfrlem5  24260  tfrALTlem  24276  welb  26417  dnwech  27145  aomclem4  27154  dfac11  27160  onfrALTlem3  28309  onfrALTlem3VD  28663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-in 3159  df-ss 3166  df-po 4314  df-so 4315  df-fr 4352  df-we 4354
  Copyright terms: Public domain W3C validator