Theorem weso 5654

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

This proof depends on syntax axioms:   → wi 4   Or wor 5570   Fr wfr 5613   We wwe 5615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-we 5618

This theorem is used by:  wecmpep  5655  wetrep  5656  wereu  5659  wereu2  5660  tz6.26  6352  wfi  6354  wfisg  6356  wfis2fg  6358  weniso  7363  wexp  8132  wfrfun  8326  wfrresex  8327  wfr2a  8328  wfr1  8329  on2recsfn  8659  on2recsov  8660  on2ind  8661  on3ind  8662  ordunifi  9257  ordtypelem7  9493  ordtypelem8  9494  hartogslem1  9511  wofib  9514  wemapso  9520  oemapso  9658  cantnf  9669  ween  10035  cflim2  10262  fin23lem27  10327  zorn2lem1  10495  zorn2lem4  10498  fpwwe2lem11  10643  fpwwe2lem12  10644  fpwwe2  10645  canth4  10649  canthwelem  10652  pwfseqlem4  10664  ltsopi  10890  ons2ind  28521  wzel  36353  wsuccl  36356  wsuclb  36357  weiunfrlem  37034  weiunpo  37035  weiunso  37036  weiunwe  37039  welb  38447  wepwso  43830  fnwe2lem3  43839  onsupuni  44016  oninfint  44023  epsoon  44040  epirron  44041  oneptr  44042  wessf1ornlem  45963