Theorem wefr 5639

Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)

Assertion

Ref	Expression
wefr	⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Proof of Theorem wefr

Step	Hyp	Ref	Expression
1		df-we 5604	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 500	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Syntax hints:   → wi 4   Or wor 5556   Fr wfr 5599   We wwe 5601

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 209  df-an 400  df-we 5604

This theorem is referenced by:  wefrc  5643  wereu  5645  wereu2  5646  tz6.26  6336  wfi  6338  wfisg  6340  wfis2fg  6342  ordfr  6363  wexp  8112  wfrfun  8306  wfrresex  8307  wfr2a  8308  wfr1  8309  wofib  9495  wemapso  9501  wemapso2lem  9502  cflim2  10222  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  ons2ind  28370  weiunwe  36834  welb  38240  fnwe2lem2  43633  onfrALTlem3  45125  onfrALTlem3VD  45467