Theorem weso 5609

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

Syntax hints:   → wi 4   Or wor 5525   Fr wfr 5568   We wwe 5570

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 208  df-an 397  df-we 5573

This theorem is referenced by:  wecmpep  5610  wetrep  5611  wereu  5614  wereu2  5615  tz6.26  6298  wfi  6300  wfisg  6302  wfis2fg  6304  weniso  7298  wexp  8070  wfrfun  8263  wfrresex  8264  wfr2a  8265  wfr1  8266  on2recsfn  8593  on2recsov  8594  on2ind  8595  on3ind  8596  ordunifi  9190  ordtypelem7  9429  ordtypelem8  9430  hartogslem1  9447  wofib  9450  wemapso  9456  oemapso  9594  cantnf  9605  ween  9948  cflim2  10176  fin23lem27  10241  zorn2lem1  10409  zorn2lem4  10412  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  canth4  10561  canthwelem  10564  pwfseqlem4  10576  ltsopi  10802  ons2ind  28285  wzel  36050  wsuccl  36053  wsuclb  36054  weiunfrlem  36692  weiunpo  36693  weiunso  36694  weiunwe  36697  welb  38103  wepwso  43488  fnwe2lem3  43497  onsupuni  43674  oninfint  43681  epsoon  43698  epirron  43699  oneptr  43700  wessf1ornlem  45632