Theorem weso 5679

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

Syntax hints:   → wi 4   Or wor 5595   Fr wfr 5637   We wwe 5639

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 5642

This theorem is referenced by:  wecmpep  5680  wetrep  5681  wereu  5684  wereu2  5685  tz6.26  6369  wfi  6372  wfisg  6375  wfis2fg  6378  weniso  7373  wexp  8153  wfrlem10OLD  8356  wfrfun  8370  wfrresex  8371  wfr2a  8372  wfr1  8373  on2recsfn  8703  on2recsov  8704  on2ind  8705  on3ind  8706  ordunifi  9323  ordtypelem7  9561  ordtypelem8  9562  hartogslem1  9579  wofib  9582  wemapso  9588  oemapso  9719  cantnf  9730  ween  10072  cflim2  10300  fin23lem27  10365  zorn2lem1  10533  zorn2lem4  10536  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  canth4  10684  canthwelem  10687  pwfseqlem4  10699  ltsopi  10925  wzel  35805  wsuccl  35808  wsuclb  35809  weiunfrlem  36446  weiunpo  36447  weiunso  36448  weiunwe  36451  welb  37722  wepwso  43031  fnwe2lem3  43040  onsupuni  43217  oninfint  43224  epsoon  43241  epirron  43242  oneptr  43243  wessf1ornlem  45127