Theorem weso 5610

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

Syntax hints:   → wi 4   Or wor 5526   Fr wfr 5569   We wwe 5571

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 207  df-an 396  df-we 5574

This theorem is referenced by:  wecmpep  5611  wetrep  5612  wereu  5615  wereu2  5616  tz6.26  6295  wfi  6297  wfisg  6299  wfis2fg  6301  weniso  7291  wexp  8063  wfrfun  8256  wfrresex  8257  wfr2a  8258  wfr1  8259  on2recsfn  8585  on2recsov  8586  on2ind  8587  on3ind  8588  ordunifi  9179  ordtypelem7  9416  ordtypelem8  9417  hartogslem1  9434  wofib  9437  wemapso  9443  oemapso  9578  cantnf  9589  ween  9929  cflim2  10157  fin23lem27  10222  zorn2lem1  10390  zorn2lem4  10393  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  canth4  10541  canthwelem  10544  pwfseqlem4  10556  ltsopi  10782  wzel  35808  wsuccl  35811  wsuclb  35812  weiunfrlem  36448  weiunpo  36449  weiunso  36450  weiunwe  36453  welb  37726  wepwso  43026  fnwe2lem3  43035  onsupuni  43212  oninfint  43219  epsoon  43236  epirron  43237  oneptr  43238  wessf1ornlem  45173