Theorem weso 5398

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

Syntax hints:   → wi 4   Or wor 5325   Fr wfr 5363   We wwe 5365

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 199  df-an 388  df-we 5368

This theorem is referenced by:  wecmpep  5399  wetrep  5400  wereu  5403  wereu2  5404  weniso  6930  wexp  7629  wfrlem10  7768  ordunifi  8563  ordtypelem7  8783  ordtypelem8  8784  hartogslem1  8801  wofib  8804  wemapso  8810  oemapso  8939  cantnf  8950  ween  9255  cflim2  9483  fin23lem27  9548  zorn2lem1  9716  zorn2lem4  9719  fpwwe2lem12  9861  fpwwe2lem13  9862  fpwwe2  9863  canth4  9867  canthwelem  9870  pwfseqlem4  9882  ltsopi  10108  wzel  32629  wsuccl  32632  wsuclb  32633  welb  34450  wepwso  39036  fnwe2lem3  39045  wessf1ornlem  40867