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

Theorem wess 4561
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 4541 . . 3  |-  ( A 
C_  B  ->  ( R  Fr  B  ->  R  Fr  A ) )
2 soss 4513 . . 3  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
31, 2anim12d 547 . 2  |-  ( A 
C_  B  ->  (
( R  Fr  B  /\  R  Or  B
)  ->  ( R  Fr  A  /\  R  Or  A ) ) )
4 df-we 4535 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
5 df-we 4535 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
63, 4, 53imtr4g 262 1  |-  ( A 
C_  B  ->  ( R  We  B  ->  R  We  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3312    Or wor 4494    Fr wfr 4530    We wwe 4532
This theorem is referenced by:  wefrc  4568  trssord  4590  ordelord  4595  fnwelem  6452  ordtypelem8  7483  oismo  7498  cantnfcl  7611  infxpenlem  7884  ac10ct  7904  dfac12lem2  8013  cflim2  8132  cofsmo  8138  hsmexlem1  8295  smobeth  8450  canthwelem  8514  gruina  8682  ltwefz  11291  omsinds  25474  wfrlem5  25515  tfrALTlem  25531  welb  26375  dnwech  27060  aomclem4  27069  dfac11  27075  onfrALTlem3  28485  onfrALTlem3VD  28853
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-in 3319  df-ss 3326  df-po 4495  df-so 4496  df-fr 4533  df-we 4535
  Copyright terms: Public domain W3C validator