Theorem weso 5542

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

Syntax hints:   → wi 4   Or wor 5467   Fr wfr 5506   We wwe 5508

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 210  df-an 400  df-we 5511

This theorem is referenced by:  wecmpep  5543  wetrep  5544  wereu  5547  wereu2  5548  weniso  7163  wexp  7897  wfrlem10  8064  ordunifi  8921  ordtypelem7  9140  ordtypelem8  9141  hartogslem1  9158  wofib  9161  wemapso  9167  oemapso  9297  cantnf  9308  ween  9649  cflim2  9877  fin23lem27  9942  zorn2lem1  10110  zorn2lem4  10113  fpwwe2lem11  10255  fpwwe2lem12  10256  fpwwe2  10257  canth4  10261  canthwelem  10264  pwfseqlem4  10276  ltsopi  10502  wzel  33555  wsuccl  33558  wsuclb  33559  on2recsfn  33563  on2recsov  33564  on2ind  33565  on3ind  33566  welb  35631  wepwso  40571  fnwe2lem3  40580  wessf1ornlem  42395