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

Theorem wess 5576
Description: Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.)
Assertion
Ref Expression
wess (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))

Proof of Theorem wess
StepHypRef Expression
1 frss 5556 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5523 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 609 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5546 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5546 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3887   Or wor 5502   Fr wfr 5541   We wwe 5543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-po 5503  df-so 5504  df-fr 5544  df-we 5546
This theorem is referenced by:  wefrc  5583  trssord  6283  ordelord  6288  omsinds  7733  omsindsOLD  7734  fnwelem  7972  wfrlem5OLD  8144  dfrecs3  8203  dfrecs3OLD  8204  ordtypelem8  9284  oismo  9299  cantnfcl  9425  infxpenlem  9769  ac10ct  9790  dfac12lem2  9900  cflim2  10019  cofsmo  10025  hsmexlem1  10182  smobeth  10342  canthwelem  10406  gruina  10574  ltwefz  13683  dford5  33671  welb  35894  dnwech  40873  aomclem4  40882  dfac11  40887  onfrALTlem3  42164  onfrALTlem3VD  42507
  Copyright terms: Public domain W3C validator