Theorem wefr 5637

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 5602	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 502	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

This proof depends on syntax axioms:   → wi 4   Or wor 5554   Fr wfr 5597   We wwe 5599

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 5602

This theorem is used by:  wefrc  5641  wereu  5643  wereu2  5644  tz6.26  6339  wfi  6341  wfisg  6343  wfis2fg  6345  ordfr  6366  wexp  8125  wfrfun  8319  wfrresex  8320  wfr2a  8321  wfr1  8322  wofib  9517  wemapso  9523  wemapso2lem  9524  cflim2  10312  fpwwe2lem11  10697  fpwwe2lem12  10698  fpwwe2  10699  ons2ind  28594  weiunwe  37179  welb  38590  fnwe2lem2  43996  onfrALTlem3  45471  onfrALTlem3VD  45813