Theorem weso 5579

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

Syntax hints:   → wi 4   Or wor 5501   Fr wfr 5540   We wwe 5542

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 206  df-an 396  df-we 5545

This theorem is referenced by:  wecmpep  5580  wetrep  5581  wereu  5584  wereu2  5585  tz6.26  6247  wfi  6250  wfisg  6253  wfis2fg  6256  weniso  7218  wexp  7955  wfrlem10OLD  8133  wfrfun  8147  wfrresex  8148  wfr2a  8149  wfr1  8150  ordunifi  9025  ordtypelem7  9244  ordtypelem8  9245  hartogslem1  9262  wofib  9265  wemapso  9271  oemapso  9401  cantnf  9412  ween  9775  cflim2  10003  fin23lem27  10068  zorn2lem1  10236  zorn2lem4  10239  fpwwe2lem11  10381  fpwwe2lem12  10382  fpwwe2  10383  canth4  10387  canthwelem  10390  pwfseqlem4  10402  ltsopi  10628  wzel  33797  wsuccl  33800  wsuclb  33801  on2recsfn  33805  on2recsov  33806  on2ind  33807  on3ind  33808  welb  35873  wepwso  40848  fnwe2lem3  40857  wessf1ornlem  42675