Theorem weso 5540

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

Syntax hints:   → wi 4   Or wor 5467   Fr wfr 5505   We wwe 5507

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 5510

This theorem is referenced by:  wecmpep  5541  wetrep  5542  wereu  5545  wereu2  5546  weniso  7101  wexp  7818  wfrlem10  7958  ordunifi  8762  ordtypelem7  8982  ordtypelem8  8983  hartogslem1  9000  wofib  9003  wemapso  9009  oemapso  9139  cantnf  9150  ween  9455  cflim2  9679  fin23lem27  9744  zorn2lem1  9912  zorn2lem4  9915  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  canth4  10063  canthwelem  10066  pwfseqlem4  10078  ltsopi  10304  wzel  33106  wsuccl  33109  wsuclb  33110  welb  35005  wepwso  39636  fnwe2lem3  39645  wessf1ornlem  41438