Theorem weso 5646

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

This proof depends on syntax axioms:   → wi 4   Or wor 5562   Fr wfr 5605   We wwe 5607

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 5610

This theorem is used by:  wecmpep  5647  wetrep  5648  wereu  5651  wereu2  5652  tz6.26  6345  wfi  6347  wfisg  6349  wfis2fg  6351  weniso  7358  wexp  8129  wfrfun  8323  wfrresex  8324  wfr2a  8325  wfr1  8326  on2recsfn  8656  on2recsov  8657  on2ind  8658  on3ind  8659  ordunifi  9261  ordtypelem7  9497  ordtypelem8  9498  hartogslem1  9515  wofib  9518  wemapso  9524  oemapso  9662  cantnf  9673  ween  10039  cflim2  10266  fin23lem27  10331  zorn2lem1  10499  zorn2lem4  10502  fpwwe2lem11  10651  fpwwe2lem12  10652  fpwwe2  10653  canth4  10657  canthwelem  10660  pwfseqlem4  10672  ltsopi  10898  ons2ind  28541  wzel  36402  wsuccl  36405  wsuclb  36406  weiunfrlem  37084  weiunpo  37085  weiunso  37086  weiunwe  37089  welb  38487  wepwso  43885  fnwe2lem3  43894  onsupuni  44071  oninfint  44078  epsoon  44095  epirron  44096  oneptr  44097  wessf1ornlem  46018