Theorem weso 5629

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

Syntax hints:   → wi 4   Or wor 5545   Fr wfr 5588   We wwe 5590

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 5593

This theorem is referenced by:  wecmpep  5630  wetrep  5631  wereu  5634  wereu2  5635  tz6.26  6320  wfi  6322  wfisg  6324  wfis2fg  6326  weniso  7329  wexp  8109  wfrfun  8302  wfrresex  8303  wfr2a  8304  wfr1  8305  on2recsfn  8631  on2recsov  8632  on2ind  8633  on3ind  8634  ordunifi  9237  ordtypelem7  9477  ordtypelem8  9478  hartogslem1  9495  wofib  9498  wemapso  9504  oemapso  9635  cantnf  9646  ween  9988  cflim2  10216  fin23lem27  10281  zorn2lem1  10449  zorn2lem4  10452  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  canthwelem  10603  pwfseqlem4  10615  ltsopi  10841  wzel  35812  wsuccl  35815  wsuclb  35816  weiunfrlem  36452  weiunpo  36453  weiunso  36454  weiunwe  36457  welb  37730  wepwso  43032  fnwe2lem3  43041  onsupuni  43218  oninfint  43225  epsoon  43242  epirron  43243  oneptr  43244  wessf1ornlem  45179