Theorem weso 5653

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

Syntax hints:   → wi 4   Or wor 5569   Fr wfr 5612   We wwe 5614

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 210  df-an 401  df-we 5617

This theorem is referenced by:  wecmpep  5654  wetrep  5655  wereu  5658  wereu2  5659  tz6.26  6349  wfi  6351  wfisg  6353  wfis2fg  6355  weniso  7353  wexp  8125  wfrfun  8319  wfrresex  8320  wfr2a  8321  wfr1  8322  on2recsfn  8652  on2recsov  8653  on2ind  8654  on3ind  8655  ordunifi  9249  ordtypelem7  9485  ordtypelem8  9486  hartogslem1  9503  wofib  9506  wemapso  9512  oemapso  9650  cantnf  9661  ween  10018  cflim2  10246  fin23lem27  10311  zorn2lem1  10479  zorn2lem4  10482  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  canth4  10631  canthwelem  10634  pwfseqlem4  10646  ltsopi  10872  ons2ind  28433  wzel  36212  wsuccl  36215  wsuclb  36216  weiunfrlem  36863  weiunpo  36864  weiunso  36865  weiunwe  36868  welb  38274  wepwso  43661  fnwe2lem3  43670  onsupuni  43847  oninfint  43854  epsoon  43871  epirron  43872  oneptr  43873  wessf1ornlem  45794