Theorem weso 5134

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

Syntax hints:   → wi 4   Or wor 5063   Fr wfr 5099   We wwe 5101

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 385  df-we 5104

This theorem is referenced by:  wecmpep  5135  wetrep  5136  wereu  5139  wereu2  5140  weniso  6644  wexp  7336  wfrlem10  7469  ordunifi  8251  ordtypelem7  8470  ordtypelem8  8471  hartogslem1  8488  wofib  8491  wemapso  8497  oemapso  8617  cantnf  8628  ween  8896  cflim2  9123  fin23lem27  9188  zorn2lem1  9356  zorn2lem4  9359  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  canth4  9507  canthwelem  9510  pwfseqlem4  9522  ltsopi  9748  wzel  31894  wsuccl  31897  wsuclb  31898  welb  33661  wepwso  37930  fnwe2lem3  37939  wessf1ornlem  39685