Theorem weso 5665

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

Syntax hints:   → wi 4   Or wor 5585   Fr wfr 5626   We wwe 5628

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 206  df-an 395  df-we 5631

This theorem is referenced by:  wecmpep  5666  wetrep  5667  wereu  5670  wereu2  5671  tz6.26  6352  wfi  6355  wfisg  6358  wfis2fg  6361  weniso  7358  wexp  8136  wfrlem10OLD  8340  wfrfun  8354  wfrresex  8355  wfr2a  8356  wfr1  8357  on2recsfn  8689  on2recsov  8690  on2ind  8691  on3ind  8692  ordunifi  9320  ordtypelem7  9560  ordtypelem8  9561  hartogslem1  9578  wofib  9581  wemapso  9587  oemapso  9718  cantnf  9729  ween  10071  cflim2  10297  fin23lem27  10362  zorn2lem1  10530  zorn2lem4  10533  fpwwe2lem11  10675  fpwwe2lem12  10676  fpwwe2  10677  canth4  10681  canthwelem  10684  pwfseqlem4  10696  ltsopi  10922  wzel  35661  wsuccl  35664  wsuclb  35665  welb  37450  wepwso  42741  fnwe2lem3  42750  onsupuni  42931  oninfint  42938  epsoon  42955  epirron  42956  oneptr  42957  wessf1ornlem  44828