Theorem weso 5668

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

Syntax hints:   → wi 4   Or wor 5588   Fr wfr 5629   We wwe 5631

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 398  df-we 5634

This theorem is referenced by:  wecmpep  5669  wetrep  5670  wereu  5673  wereu2  5674  tz6.26  6349  wfi  6352  wfisg  6355  wfis2fg  6358  weniso  7351  wexp  8116  wfrlem10OLD  8318  wfrfun  8332  wfrresex  8333  wfr2a  8334  wfr1  8335  on2recsfn  8666  on2recsov  8667  on2ind  8668  on3ind  8669  ordunifi  9293  ordtypelem7  9519  ordtypelem8  9520  hartogslem1  9537  wofib  9540  wemapso  9546  oemapso  9677  cantnf  9688  ween  10030  cflim2  10258  fin23lem27  10323  zorn2lem1  10491  zorn2lem4  10494  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  canth4  10642  canthwelem  10645  pwfseqlem4  10657  ltsopi  10883  wzel  34796  wsuccl  34799  wsuclb  34800  welb  36604  wepwso  41785  fnwe2lem3  41794  onsupuni  41978  oninfint  41985  epsoon  42002  epirron  42003  oneptr  42004  wessf1ornlem  43882