Theorem weso 5105

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

Syntax hints:   → wi 4   Or wor 5034   Fr wfr 5070   We wwe 5072

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 197  df-an 386  df-we 5075

This theorem is referenced by:  wecmpep  5106  wetrep  5107  wereu  5110  wereu2  5111  weniso  6604  wexp  7291  wfrlem10  7424  ordunifi  8210  ordtypelem7  8429  ordtypelem8  8430  hartogslem1  8447  wofib  8450  wemapso  8456  oemapso  8579  cantnf  8590  ween  8858  cflim2  9085  fin23lem27  9150  zorn2lem1  9318  zorn2lem4  9321  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  canthwelem  9472  pwfseqlem4  9484  ltsopi  9710  wzel  31771  wzelOLD  31772  wsuccl  31776  wsuclb  31777  welb  33531  wepwso  37613  fnwe2lem3  37622  wessf1ornlem  39371