Theorem weso 5642

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

This proof depends on syntax axioms:   → wi 4   Or wor 5558   Fr wfr 5601   We wwe 5603

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 5606

This theorem is used by:  wecmpep  5643  wetrep  5644  wereu  5647  wereu2  5648  tz6.26  6350  wfi  6352  wfisg  6354  wfis2fg  6356  weniso  7364  wexp  8142  fnwe2lem4  8148  wfrfun  8341  wfrresex  8342  wfr2a  8343  wfr1  8344  on2recsfn  8676  on2recsov  8677  on2ind  8678  on3ind  8679  ordunifi  9281  ordtypelem7  9518  ordtypelem8  9519  hartogslem1  9536  wofib  9539  wemapso  9545  oemapso  9683  cantnf  9694  ween  10114  cflim2  10341  fin23lem27  10406  zorn2lem1  10574  zorn2lem4  10577  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  canth4  10732  canthwelem  10735  pwfseqlem4  10747  ltsopi  10973  ons2ind  28661  weexenwe  35756  wzel  36586  wsuccl  36589  wsuclb  36590  weiunfrlem  37252  weiunpo  37253  weiunso  37254  weiunwe  37257  welb  38670  wepwso  44049  onsupuni  44230  oninfint  44237  epsoon  44254  epirron  44255  oneptr  44256  wessf1ornlem  46199