Theorem weso 5616

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

Syntax hints:   → wi 4   Or wor 5532   Fr wfr 5575   We wwe 5577

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 5580

This theorem is referenced by:  wecmpep  5617  wetrep  5618  wereu  5621  wereu2  5622  tz6.26  6306  wfi  6308  wfisg  6310  wfis2fg  6312  weniso  7303  wexp  8074  wfrfun  8267  wfrresex  8268  wfr2a  8269  wfr1  8270  on2recsfn  8597  on2recsov  8598  on2ind  8599  on3ind  8600  ordunifi  9194  ordtypelem7  9433  ordtypelem8  9434  hartogslem1  9451  wofib  9454  wemapso  9460  oemapso  9597  cantnf  9608  ween  9951  cflim2  10179  fin23lem27  10244  zorn2lem1  10412  zorn2lem4  10415  fpwwe2lem11  10558  fpwwe2lem12  10559  fpwwe2  10560  canth4  10564  canthwelem  10567  pwfseqlem4  10579  ltsopi  10805  ons2ind  28284  wzel  36023  wsuccl  36026  wsuclb  36027  weiunfrlem  36665  weiunpo  36666  weiunso  36667  weiunwe  36670  welb  38074  wepwso  43492  fnwe2lem3  43501  onsupuni  43678  oninfint  43685  epsoon  43702  epirron  43703  oneptr  43704  wessf1ornlem  45636