Theorem weso 5029

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

Syntax hints:   → wi 4   Or wor 4958   Fr wfr 4994   We wwe 4996

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 196  df-an 385  df-we 4999

This theorem is referenced by:  wecmpep  5030  wetrep  5031  wereu  5034  wereu2  5035  weniso  6504  wexp  7178  wfrlem10  7311  ordunifi  8095  ordtypelem7  8312  ordtypelem8  8313  hartogslem1  8330  wofib  8333  wemapso  8339  oemapso  8462  cantnf  8473  ween  8741  cflim2  8968  fin23lem27  9033  zorn2lem1  9201  zorn2lem4  9204  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  canth4  9348  canthwelem  9351  pwfseqlem4  9363  ltsopi  9589  wzel  31015  wzelOLD  31016  wsuccl  31020  wsuclb  31021  welb  32701  wepwso  36631  fnwe2lem3  36640  wessf1ornlem  38366