Theorem weso 5676

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

Syntax hints:   → wi 4   Or wor 5591   Fr wfr 5634   We wwe 5636

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 5639

This theorem is referenced by:  wecmpep  5677  wetrep  5678  wereu  5681  wereu2  5682  tz6.26  6368  wfi  6371  wfisg  6374  wfis2fg  6377  weniso  7374  wexp  8155  wfrlem10OLD  8358  wfrfun  8372  wfrresex  8373  wfr2a  8374  wfr1  8375  on2recsfn  8705  on2recsov  8706  on2ind  8707  on3ind  8708  ordunifi  9326  ordtypelem7  9564  ordtypelem8  9565  hartogslem1  9582  wofib  9585  wemapso  9591  oemapso  9722  cantnf  9733  ween  10075  cflim2  10303  fin23lem27  10368  zorn2lem1  10536  zorn2lem4  10539  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  canth4  10687  canthwelem  10690  pwfseqlem4  10702  ltsopi  10928  wzel  35825  wsuccl  35828  wsuclb  35829  weiunfrlem  36465  weiunpo  36466  weiunso  36467  weiunwe  36470  welb  37743  wepwso  43055  fnwe2lem3  43064  onsupuni  43241  oninfint  43248  epsoon  43265  epirron  43266  oneptr  43267  wessf1ornlem  45190