Theorem weso 5622

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

Syntax hints:   → wi 4   Or wor 5538   Fr wfr 5581   We wwe 5583

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 5586

This theorem is referenced by:  wecmpep  5623  wetrep  5624  wereu  5627  wereu2  5628  tz6.26  6308  wfi  6310  wfisg  6312  wfis2fg  6314  weniso  7311  wexp  8086  wfrfun  8279  wfrresex  8280  wfr2a  8281  wfr1  8282  on2recsfn  8608  on2recsov  8609  on2ind  8610  on3ind  8611  ordunifi  9213  ordtypelem7  9453  ordtypelem8  9454  hartogslem1  9471  wofib  9474  wemapso  9480  oemapso  9611  cantnf  9622  ween  9964  cflim2  10192  fin23lem27  10257  zorn2lem1  10425  zorn2lem4  10428  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  canth4  10576  canthwelem  10579  pwfseqlem4  10591  ltsopi  10817  wzel  35805  wsuccl  35808  wsuclb  35809  weiunfrlem  36445  weiunpo  36446  weiunso  36447  weiunwe  36450  welb  37723  wepwso  43025  fnwe2lem3  43034  onsupuni  43211  oninfint  43218  epsoon  43235  epirron  43236  oneptr  43237  wessf1ornlem  45172