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  6353  wfi  6355  wfisg  6357  wfis2fg  6359  weniso  7368  wexp  8149  fnwe2lem4  8155  wfrfun  8349  wfrresex  8350  wfr2a  8351  wfr1  8352  on2recsfn  8684  on2recsov  8685  on2ind  8686  on3ind  8687  ordunifi  9289  ordtypelem7  9525  ordtypelem8  9526  hartogslem1  9543  wofib  9546  wemapso  9552  oemapso  9690  cantnf  9701  ween  10121  cflim2  10348  fin23lem27  10413  zorn2lem1  10581  zorn2lem4  10584  fpwwe2lem11  10733  fpwwe2lem12  10734  fpwwe2  10735  canth4  10739  canthwelem  10742  pwfseqlem4  10754  ltsopi  10980  ons2ind  28670  weexenwe  35824  wzel  36710  wsuccl  36713  wsuclb  36714  weiunfrlem  37376  weiunpo  37377  weiunso  37378  weiunwe  37381  welb  38807  wepwso  44187  onsupuni  44368  oninfint  44375  epsoon  44392  epirron  44393  oneptr  44394  wessf1ornlem  46336