Theorem weso 5613

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

Syntax hints:   → wi 4   Or wor 5529   Fr wfr 5572   We wwe 5574

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 5577

This theorem is referenced by:  wecmpep  5614  wetrep  5615  wereu  5618  wereu2  5619  tz6.26  6303  wfi  6305  wfisg  6307  wfis2fg  6309  weniso  7298  wexp  8070  wfrfun  8263  wfrresex  8264  wfr2a  8265  wfr1  8266  on2recsfn  8593  on2recsov  8594  on2ind  8595  on3ind  8596  ordunifi  9188  ordtypelem7  9427  ordtypelem8  9428  hartogslem1  9445  wofib  9448  wemapso  9454  oemapso  9589  cantnf  9600  ween  9943  cflim2  10171  fin23lem27  10236  zorn2lem1  10404  zorn2lem4  10407  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe2  10552  canth4  10556  canthwelem  10559  pwfseqlem4  10571  ltsopi  10797  wzel  35965  wsuccl  35968  wsuclb  35969  weiunfrlem  36607  weiunpo  36608  weiunso  36609  weiunwe  36612  welb  37876  wepwso  43227  fnwe2lem3  43236  onsupuni  43413  oninfint  43420  epsoon  43437  epirron  43438  oneptr  43439  wessf1ornlem  45371