Theorem weso 5652

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

Syntax hints:   → wi 4   Or wor 5568   Fr wfr 5611   We wwe 5613

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 210  df-an 401  df-we 5616

This theorem is referenced by:  wecmpep  5653  wetrep  5654  wereu  5657  wereu2  5658  tz6.26  6348  wfi  6350  wfisg  6352  wfis2fg  6354  weniso  7352  wexp  8122  wfrfun  8316  wfrresex  8317  wfr2a  8318  wfr1  8319  on2recsfn  8649  on2recsov  8650  on2ind  8651  on3ind  8652  ordunifi  9246  ordtypelem7  9482  ordtypelem8  9483  hartogslem1  9500  wofib  9503  wemapso  9509  oemapso  9647  cantnf  9658  ween  10015  cflim2  10242  fin23lem27  10307  zorn2lem1  10475  zorn2lem4  10478  fpwwe2lem11  10621  fpwwe2lem12  10622  fpwwe2  10623  canth4  10627  canthwelem  10630  pwfseqlem4  10642  ltsopi  10868  ons2ind  28468  wzel  36314  wsuccl  36317  wsuclb  36318  weiunfrlem  36975  weiunpo  36976  weiunso  36977  weiunwe  36980  welb  38387  wepwso  43770  fnwe2lem3  43779  onsupuni  43956  oninfint  43963  epsoon  43980  epirron  43981  oneptr  43982  wessf1ornlem  45903