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

Theorem wess 5297
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 5277 . . 3 (𝐴𝐵 → (𝑅 Fr 𝐵𝑅 Fr 𝐴))
2 soss 5249 . . 3 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
31, 2anim12d 603 . 2 (𝐴𝐵 → ((𝑅 Fr 𝐵𝑅 Or 𝐵) → (𝑅 Fr 𝐴𝑅 Or 𝐴)))
4 df-we 5271 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
5 df-we 5271 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
63, 4, 53imtr4g 288 1 (𝐴𝐵 → (𝑅 We 𝐵𝑅 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wss 3767   Or wor 5230   Fr wfr 5266   We wwe 5268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-ral 3092  df-in 3774  df-ss 3781  df-po 5231  df-so 5232  df-fr 5269  df-we 5271
This theorem is referenced by:  wefrc  5304  trssord  5956  ordelord  5961  omsinds  7316  fnwelem  7527  wfrlem5  7656  dfrecs3  7706  ordtypelem8  8670  oismo  8685  cantnfcl  8812  infxpenlem  9120  ac10ct  9141  dfac12lem2  9252  cflim2  9371  cofsmo  9377  hsmexlem1  9534  smobeth  9694  canthwelem  9758  gruina  9926  ltwefz  13013  dford5  32115  welb  34011  dnwech  38391  aomclem4  38400  dfac11  38405  onfrALTlem3  39518  onfrALTlem3VD  39871
  Copyright terms: Public domain W3C validator