Theorem weso 5623

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

Syntax hints:   → wi 4   Or wor 5539   Fr wfr 5582   We wwe 5584

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 207  df-an 396  df-we 5587

This theorem is referenced by:  wecmpep  5624  wetrep  5625  wereu  5628  wereu2  5629  tz6.26  6313  wfi  6315  wfisg  6317  wfis2fg  6319  weniso  7310  wexp  8082  wfrfun  8275  wfrresex  8276  wfr2a  8277  wfr1  8278  on2recsfn  8605  on2recsov  8606  on2ind  8607  on3ind  8608  ordunifi  9202  ordtypelem7  9441  ordtypelem8  9442  hartogslem1  9459  wofib  9462  wemapso  9468  oemapso  9603  cantnf  9614  ween  9957  cflim2  10185  fin23lem27  10250  zorn2lem1  10418  zorn2lem4  10421  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  canthwelem  10573  pwfseqlem4  10585  ltsopi  10811  ons2ind  28283  wzel  36038  wsuccl  36041  wsuclb  36042  weiunfrlem  36680  weiunpo  36681  weiunso  36682  weiunwe  36685  welb  37987  wepwso  43400  fnwe2lem3  43409  onsupuni  43586  oninfint  43593  epsoon  43610  epirron  43611  oneptr  43612  wessf1ornlem  45544