Theorem weso 5615

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

Syntax hints:   → wi 4   Or wor 5531   Fr wfr 5574   We wwe 5576

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 5579

This theorem is referenced by:  wecmpep  5616  wetrep  5617  wereu  5620  wereu2  5621  tz6.26  6305  wfi  6307  wfisg  6309  wfis2fg  6311  weniso  7300  wexp  8072  wfrfun  8265  wfrresex  8266  wfr2a  8267  wfr1  8268  on2recsfn  8595  on2recsov  8596  on2ind  8597  on3ind  8598  ordunifi  9190  ordtypelem7  9429  ordtypelem8  9430  hartogslem1  9447  wofib  9450  wemapso  9456  oemapso  9591  cantnf  9602  ween  9945  cflim2  10173  fin23lem27  10238  zorn2lem1  10406  zorn2lem4  10409  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  canth4  10558  canthwelem  10561  pwfseqlem4  10573  ltsopi  10799  ons2ind  28271  wzel  36016  wsuccl  36019  wsuclb  36020  weiunfrlem  36658  weiunpo  36659  weiunso  36660  weiunwe  36663  welb  37937  wepwso  43285  fnwe2lem3  43294  onsupuni  43471  oninfint  43478  epsoon  43495  epirron  43496  oneptr  43497  wessf1ornlem  45429