Theorem weso 5649

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

This proof depends on syntax axioms:   → wi 4   Or wor 5565   Fr wfr 5608   We wwe 5610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-we 5613

This theorem is used by:  wecmpep  5650  wetrep  5651  wereu  5654  wereu2  5655  welb  6317  tz6.26  6376  wfi  6378  wfisg  6380  wfis2fg  6382  weniso  7395  wexp  8179  fnwe2lem4  8185  wfrfun  8379  wfrresex  8380  wfr2a  8381  wfr1  8382  on2recsfn  8714  on2recsov  8715  on2ind  8716  on3ind  8717  ordunifi  9319  ordtypelem7  9555  ordtypelem8  9556  hartogslem1  9573  wofib  9576  wemapso  9582  oemapso  9720  cantnf  9731  ween  10153  cflim2  10380  fin23lem27  10445  zorn2lem1  10613  zorn2lem4  10616  fpwwe2lem11  10765  fpwwe2lem12  10766  fpwwe2  10767  canth4  10771  canthwelem  10774  pwfseqlem4  10786  ltsopi  11012  ons2ind  28718  weinfcl  33636  weinflb  33637  weexenwe  35889  wzel  36801  wsuccl  36804  wsuclb  36805  weiunfrlem  37467  weiunpo  37468  weiunso  37469  weiunwe  37472  wepwso  44316  onsupuni  44492  oninfint  44499  epsoon  44516  epirron  44517  oneptr  44518  wessf1ornlem  46473