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

Syntax hints:   → wi 4   Or wor 5549   Fr wfr 5590   We wwe 5592

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 397  df-we 5595

This theorem is referenced by:  wecmpep  5630  wetrep  5631  wereu  5634  wereu2  5635  tz6.26  6306  wfi  6309  wfisg  6312  wfis2fg  6315  weniso  7304  wexp  8067  wfrlem10OLD  8269  wfrfun  8283  wfrresex  8284  wfr2a  8285  wfr1  8286  on2recsfn  8618  on2recsov  8619  on2ind  8620  on3ind  8621  ordunifi  9244  ordtypelem7  9469  ordtypelem8  9470  hartogslem1  9487  wofib  9490  wemapso  9496  oemapso  9627  cantnf  9638  ween  9980  cflim2  10208  fin23lem27  10273  zorn2lem1  10441  zorn2lem4  10444  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  canth4  10592  canthwelem  10595  pwfseqlem4  10607  ltsopi  10833  wzel  34485  wsuccl  34488  wsuclb  34489  welb  36268  wepwso  41428  fnwe2lem3  41437  onsupuni  41621  oninfint  41628  epsoon  41645  epirron  41646  oneptr  41647  wessf1ornlem  43525