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

Theorem wess 4317
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 4297 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4269 . . 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 4291 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4291 . 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 3094    Or wor 4250    Fr wfr 4286    We wwe 4288
This theorem is referenced by:  wefrc  4324  trssord  4346  ordelord  4351  fnwelem  6129  ordtypelem8  7173  oismo  7188  cantnfcl  7301  infxpenlem  7574  ac10ct  7594  dfac12lem2  7703  cflim2  7822  cofsmo  7828  hsmexlem1  7985  smobeth  8141  canthwelem  8205  gruina  8373  ltwefz  10957  omsinds  23553  wfrlem5  23594  tfrALTlem  23610  welb  25749  dnwech  26477  aomclem4  26486  dfac11  26492  onfrALTlem3  27325  onfrALTlem3VD  27676
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ral 2520  df-in 3101  df-ss 3108  df-po 4251  df-so 4252  df-fr 4289  df-we 4291
  Copyright terms: Public domain W3C validator