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

Theorem wess 5540
 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 5520 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5491 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 608 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5514 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5514 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 297 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3939   Or wor 5471   Fr wfr 5509   We wwe 5511 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-ral 3147  df-in 3946  df-ss 3955  df-po 5472  df-so 5473  df-fr 5512  df-we 5514 This theorem is referenced by:  wefrc  5547  trssord  6205  ordelord  6210  omsinds  7591  fnwelem  7819  wfrlem5  7953  dfrecs3  8003  ordtypelem8  8981  oismo  8996  cantnfcl  9122  infxpenlem  9431  ac10ct  9452  dfac12lem2  9562  cflim2  9677  cofsmo  9683  hsmexlem1  9840  smobeth  10000  canthwelem  10064  gruina  10232  ltwefz  13324  dford5  32843  welb  34881  dnwech  39515  aomclem4  39524  dfac11  39529  onfrALTlem3  40745  onfrALTlem3VD  41088
 Copyright terms: Public domain W3C validator