Theorem weso 5653

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 5617	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simprbi 502	1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)

Syntax hints:   → wi 4   Or wor 5569   Fr wfr 5612   We wwe 5614

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 210  df-an 401  df-we 5617

This theorem is referenced by:  wecmpep  5654  wetrep  5655  wereu  5658  wereu2  5659  tz6.26  6349  wfi  6351  wfisg  6353  wfis2fg  6355  weniso  7353  wexp  8126  wfrfun  8320  wfrresex  8321  wfr2a  8322  wfr1  8323  on2recsfn  8653  on2recsov  8654  on2ind  8655  on3ind  8656  ordunifi  9250  ordtypelem7  9486  ordtypelem8  9487  hartogslem1  9504  wofib  9507  wemapso  9513  oemapso  9651  cantnf  9662  ween  10019  cflim2  10247  fin23lem27  10312  zorn2lem1  10480  zorn2lem4  10483  fpwwe2lem11  10626  fpwwe2lem12  10627  fpwwe2  10628  canth4  10632  canthwelem  10635  pwfseqlem4  10647  ltsopi  10873  ons2ind  28434  wzel  36247  wsuccl  36250  wsuclb  36251  weiunfrlem  36898  weiunpo  36899  weiunso  36900  weiunwe  36903  welb  38309  wepwso  43696  fnwe2lem3  43705  onsupuni  43882  oninfint  43889  epsoon  43906  epirron  43907  oneptr  43908  wessf1ornlem  45829