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 497	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  6311  wfi  6313  wfisg  6315  wfis2fg  6317  weniso  7309  wexp  8080  wfrfun  8273  wfrresex  8274  wfr2a  8275  wfr1  8276  on2recsfn  8603  on2recsov  8604  on2ind  8605  on3ind  8606  ordunifi  9200  ordtypelem7  9439  ordtypelem8  9440  hartogslem1  9457  wofib  9460  wemapso  9466  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  28267  wzel  36004  wsuccl  36007  wsuclb  36008  weiunfrlem  36646  weiunpo  36647  weiunso  36648  weiunwe  36651  welb  38057  wepwso  43471  fnwe2lem3  43480  onsupuni  43657  oninfint  43664  epsoon  43681  epirron  43682  oneptr  43683  wessf1ornlem  45615