Theorem weso 5632

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

Syntax hints:   → wi 4   Or wor 5548   Fr wfr 5591   We wwe 5593

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 5596

This theorem is referenced by:  wecmpep  5633  wetrep  5634  wereu  5637  wereu2  5638  tz6.26  6323  wfi  6325  wfisg  6327  wfis2fg  6329  weniso  7332  wexp  8112  wfrfun  8305  wfrresex  8306  wfr2a  8307  wfr1  8308  on2recsfn  8634  on2recsov  8635  on2ind  8636  on3ind  8637  ordunifi  9244  ordtypelem7  9484  ordtypelem8  9485  hartogslem1  9502  wofib  9505  wemapso  9511  oemapso  9642  cantnf  9653  ween  9995  cflim2  10223  fin23lem27  10288  zorn2lem1  10456  zorn2lem4  10459  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  canth4  10607  canthwelem  10610  pwfseqlem4  10622  ltsopi  10848  wzel  35819  wsuccl  35822  wsuclb  35823  weiunfrlem  36459  weiunpo  36460  weiunso  36461  weiunwe  36464  welb  37737  wepwso  43039  fnwe2lem3  43048  onsupuni  43225  oninfint  43232  epsoon  43249  epirron  43250  oneptr  43251  wessf1ornlem  45186