Theorem weso 5605

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

Syntax hints:   → wi 4   Or wor 5521   Fr wfr 5564   We wwe 5566

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 5569

This theorem is referenced by:  wecmpep  5606  wetrep  5607  wereu  5610  wereu2  5611  tz6.26  6294  wfi  6296  wfisg  6298  wfis2fg  6300  weniso  7288  wexp  8060  wfrfun  8253  wfrresex  8254  wfr2a  8255  wfr1  8256  on2recsfn  8582  on2recsov  8583  on2ind  8584  on3ind  8585  ordunifi  9174  ordtypelem7  9410  ordtypelem8  9411  hartogslem1  9428  wofib  9431  wemapso  9437  oemapso  9572  cantnf  9583  ween  9926  cflim2  10154  fin23lem27  10219  zorn2lem1  10387  zorn2lem4  10390  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  canth4  10538  canthwelem  10541  pwfseqlem4  10553  ltsopi  10779  wzel  35866  wsuccl  35869  wsuclb  35870  weiunfrlem  36508  weiunpo  36509  weiunso  36510  weiunwe  36513  welb  37786  wepwso  43146  fnwe2lem3  43155  onsupuni  43332  oninfint  43339  epsoon  43356  epirron  43357  oneptr  43358  wessf1ornlem  45292