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

Theorem wess 4855
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 4835 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4807 . . 3  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
31, 2anim12d 561 . 2  |-  ( A 
C_  B  ->  (
( R  Fr  B  /\  R  Or  B
)  ->  ( R  Fr  A  /\  R  Or  A ) ) )
4 df-we 4829 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4829 . 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 367    C_ wss 3461    Or wor 4788    Fr wfr 4824    We wwe 4826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-in 3468  df-ss 3475  df-po 4789  df-so 4790  df-fr 4827  df-we 4829
This theorem is referenced by:  wefrc  4862  trssord  4884  ordelord  4889  fnwelem  6888  ordtypelem8  7942  oismo  7957  cantnfcl  8077  cantnfclOLD  8107  infxpenlem  8382  ac10ct  8406  dfac12lem2  8515  cflim2  8634  cofsmo  8640  hsmexlem1  8797  smobeth  8952  canthwelem  9017  gruina  9185  ltwefz  12059  omsinds  29542  wfrlem5  29590  welb  30470  dnwech  31236  aomclem4  31245  dfac11  31250  onfrALTlem3  33729  onfrALTlem3VD  34107
  Copyright terms: Public domain W3C validator