Theorem weso 5548

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

Syntax hints:   → wi 4   Or wor 5475   Fr wfr 5513   We wwe 5515

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 209  df-an 399  df-we 5518

This theorem is referenced by:  wecmpep  5549  wetrep  5550  wereu  5553  wereu2  5554  weniso  7109  wexp  7826  wfrlem10  7966  ordunifi  8770  ordtypelem7  8990  ordtypelem8  8991  hartogslem1  9008  wofib  9011  wemapso  9017  oemapso  9147  cantnf  9158  ween  9463  cflim2  9687  fin23lem27  9752  zorn2lem1  9920  zorn2lem4  9923  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  canth4  10071  canthwelem  10074  pwfseqlem4  10086  ltsopi  10312  wzel  33113  wsuccl  33116  wsuclb  33117  welb  35013  wepwso  39650  fnwe2lem3  39659  wessf1ornlem  41452