Theorem weso 5638

Description: A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.)

Assertion

Ref	Expression
weso	⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)

Proof of Theorem weso

Step	Hyp	Ref	Expression
1		df-we 5602	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simprbi 501	1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)

Syntax hints:   → wi 4   Or wor 5554   Fr wfr 5597   We wwe 5599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400  df-we 5602

This theorem is referenced by:  wecmpep  5639  wetrep  5640  wereu  5643  wereu2  5644  tz6.26  6334  wfi  6336  wfisg  6338  wfis2fg  6340  weniso  7338  wexp  8110  wfrfun  8304  wfrresex  8305  wfr2a  8306  wfr1  8307  on2recsfn  8637  on2recsov  8638  on2ind  8639  on3ind  8640  ordunifi  9234  ordtypelem7  9472  ordtypelem8  9473  hartogslem1  9490  wofib  9493  wemapso  9499  oemapso  9637  cantnf  9648  ween  9991  cflim2  10220  fin23lem27  10285  zorn2lem1  10453  zorn2lem4  10456  fpwwe2lem11  10599  fpwwe2lem12  10600  fpwwe2  10601  canth4  10605  canthwelem  10608  pwfseqlem4  10620  ltsopi  10846  ons2ind  28368  wzel  36172  wsuccl  36175  wsuclb  36176  weiunfrlem  36824  weiunpo  36825  weiunso  36826  weiunwe  36829  welb  38235  wepwso  43620  fnwe2lem3  43629  onsupuni  43806  oninfint  43813  epsoon  43830  epirron  43831  oneptr  43832  wessf1ornlem  45763