Theorem weso 5622

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

Syntax hints:   → wi 4   Or wor 5538   Fr wfr 5581   We wwe 5583

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 5586

This theorem is referenced by:  wecmpep  5623  wetrep  5624  wereu  5627  wereu2  5628  tz6.26  6308  wfi  6310  wfisg  6312  wfis2fg  6314  weniso  7311  wexp  8086  wfrfun  8279  wfrresex  8280  wfr2a  8281  wfr1  8282  on2recsfn  8608  on2recsov  8609  on2ind  8610  on3ind  8611  ordunifi  9213  ordtypelem7  9453  ordtypelem8  9454  hartogslem1  9471  wofib  9474  wemapso  9480  oemapso  9611  cantnf  9622  ween  9964  cflim2  10192  fin23lem27  10257  zorn2lem1  10425  zorn2lem4  10428  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  canth4  10576  canthwelem  10579  pwfseqlem4  10591  ltsopi  10817  wzel  35785  wsuccl  35788  wsuclb  35789  weiunfrlem  36425  weiunpo  36426  weiunso  36427  weiunwe  36430  welb  37703  wepwso  43005  fnwe2lem3  43014  onsupuni  43191  oninfint  43198  epsoon  43215  epirron  43216  oneptr  43217  wessf1ornlem  45152