Theorem weso 5605

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

Syntax hints:   → wi 4   Or wor 5525   Fr wfr 5566   We wwe 5568

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 397  df-we 5571

This theorem is referenced by:  wecmpep  5606  wetrep  5607  wereu  5610  wereu2  5611  tz6.26  6280  wfi  6283  wfisg  6286  wfis2fg  6289  weniso  7275  wexp  8030  wfrlem10OLD  8211  wfrfun  8225  wfrresex  8226  wfr2a  8227  wfr1  8228  ordunifi  9150  ordtypelem7  9373  ordtypelem8  9374  hartogslem1  9391  wofib  9394  wemapso  9400  oemapso  9531  cantnf  9542  ween  9884  cflim2  10112  fin23lem27  10177  zorn2lem1  10345  zorn2lem4  10348  fpwwe2lem11  10490  fpwwe2lem12  10491  fpwwe2  10492  canth4  10496  canthwelem  10499  pwfseqlem4  10511  ltsopi  10737  wzel  34041  wsuccl  34044  wsuclb  34045  on2recsfn  34049  on2recsov  34050  on2ind  34051  on3ind  34052  welb  35992  wepwso  41119  fnwe2lem3  41128  wessf1ornlem  43038