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 548 . 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 263 1  |-  ( A 
C_  B  ->  ( R  We  B  ->  R  We  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    C_ wss 3154    Or wor 4313    Fr wfr 4349    We wwe 4351
This theorem is referenced by:  wefrc  4387  trssord  4409  ordelord  4414  fnwelem  6192  ordtypelem8  7236  oismo  7251  cantnfcl  7364  infxpenlem  7637  ac10ct  7657  dfac12lem2  7766  cflim2  7885  cofsmo  7891  hsmexlem1  8048  smobeth  8204  canthwelem  8268  gruina  8436  ltwefz  11021  omsinds  23621  wfrlem5  23662  tfrALTlem  23678  welb  25817  dnwech  26545  aomclem4  26554  dfac11  26560  onfrALTlem3  27581  onfrALTlem3VD  27932
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-in 3161  df-ss 3168  df-po 4314  df-so 4315  df-fr 4352  df-we 4354
  Copyright terms: Public domain W3C validator