Theorem weso 5591

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

Syntax hints:   → wi 4   Or wor 5513   Fr wfr 5552   We wwe 5554

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 206  df-an 398  df-we 5557

This theorem is referenced by:  wecmpep  5592  wetrep  5593  wereu  5596  wereu2  5597  tz6.26  6265  wfi  6268  wfisg  6271  wfis2fg  6274  weniso  7257  wexp  8002  wfrlem10OLD  8180  wfrfun  8194  wfrresex  8195  wfr2a  8196  wfr1  8197  ordunifi  9108  ordtypelem7  9327  ordtypelem8  9328  hartogslem1  9345  wofib  9348  wemapso  9354  oemapso  9484  cantnf  9495  ween  9837  cflim2  10065  fin23lem27  10130  zorn2lem1  10298  zorn2lem4  10301  fpwwe2lem11  10443  fpwwe2lem12  10444  fpwwe2  10445  canth4  10449  canthwelem  10452  pwfseqlem4  10464  ltsopi  10690  wzel  33863  wsuccl  33866  wsuclb  33867  on2recsfn  33871  on2recsov  33872  on2ind  33873  on3ind  33874  welb  35938  wepwso  40906  fnwe2lem3  40915  wessf1ornlem  42766