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

Theorem wess 5130
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 5110 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5082 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 585 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5104 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5104 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 285 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wss 3607   Or wor 5063   Fr wfr 5099   We wwe 5101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-in 3614  df-ss 3621  df-po 5064  df-so 5065  df-fr 5102  df-we 5104
This theorem is referenced by:  wefrc  5137  trssord  5778  ordelord  5783  omsinds  7126  fnwelem  7337  wfrlem5  7464  dfrecs3  7514  ordtypelem8  8471  oismo  8486  cantnfcl  8602  infxpenlem  8874  ac10ct  8895  dfac12lem2  9004  cflim2  9123  cofsmo  9129  hsmexlem1  9286  smobeth  9446  canthwelem  9510  gruina  9678  ltwefz  12802  dford5  31734  welb  33661  dnwech  37935  aomclem4  37944  dfac11  37949  onfrALTlem3  39076  onfrALTlem3VD  39437
  Copyright terms: Public domain W3C validator