Theorem weso 5691

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

Syntax hints:   → wi 4   Or wor 5606   Fr wfr 5649   We wwe 5651

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 5654

This theorem is referenced by:  wecmpep  5692  wetrep  5693  wereu  5696  wereu2  5697  tz6.26  6379  wfi  6382  wfisg  6385  wfis2fg  6388  weniso  7390  wexp  8171  wfrlem10OLD  8374  wfrfun  8388  wfrresex  8389  wfr2a  8390  wfr1  8391  on2recsfn  8723  on2recsov  8724  on2ind  8725  on3ind  8726  ordunifi  9354  ordtypelem7  9593  ordtypelem8  9594  hartogslem1  9611  wofib  9614  wemapso  9620  oemapso  9751  cantnf  9762  ween  10104  cflim2  10332  fin23lem27  10397  zorn2lem1  10565  zorn2lem4  10568  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  canth4  10716  canthwelem  10719  pwfseqlem4  10731  ltsopi  10957  wzel  35788  wsuccl  35791  wsuclb  35792  weiunfrlem  36430  weiunpo  36431  weiunso  36432  weiunwe  36435  welb  37696  wepwso  43000  fnwe2lem3  43009  onsupuni  43190  oninfint  43197  epsoon  43214  epirron  43215  oneptr  43216  wessf1ornlem  45092