Theorem weso 5650

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 496	1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)

Syntax hints:   → wi 4   Or wor 5565   Fr wfr 5608   We wwe 5610

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 207  df-an 396  df-we 5613

This theorem is referenced by:  wecmpep  5651  wetrep  5652  wereu  5655  wereu2  5656  tz6.26  6341  wfi  6344  wfisg  6347  wfis2fg  6350  weniso  7352  wexp  8134  wfrlem10OLD  8337  wfrfun  8351  wfrresex  8352  wfr2a  8353  wfr1  8354  on2recsfn  8684  on2recsov  8685  on2ind  8686  on3ind  8687  ordunifi  9303  ordtypelem7  9543  ordtypelem8  9544  hartogslem1  9561  wofib  9564  wemapso  9570  oemapso  9701  cantnf  9712  ween  10054  cflim2  10282  fin23lem27  10347  zorn2lem1  10515  zorn2lem4  10518  fpwwe2lem11  10660  fpwwe2lem12  10661  fpwwe2  10662  canth4  10666  canthwelem  10669  pwfseqlem4  10681  ltsopi  10907  wzel  35847  wsuccl  35850  wsuclb  35851  weiunfrlem  36487  weiunpo  36488  weiunso  36489  weiunwe  36492  welb  37765  wepwso  43034  fnwe2lem3  43043  onsupuni  43220  oninfint  43227  epsoon  43244  epirron  43245  oneptr  43246  wessf1ornlem  45176