Theorem wefr 5650

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

This proof depends on syntax axioms:   → wi 4   Or wor 5567   Fr wfr 5610   We wwe 5612

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 401  df-we 5615

This theorem is used by:  wefrc  5654  wereu  5656  wereu2  5657  tz6.26  6348  wfi  6350  wfisg  6352  wfis2fg  6354  ordfr  6375  wexp  8124  wfrfun  8318  wfrresex  8319  wfr2a  8320  wfr1  8321  wofib  9505  wemapso  9511  wemapso2lem  9512  cflim2  10253  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  ons2ind  28479  weiunwe  37008  welb  38415  fnwe2lem2  43806  onfrALTlem3  45281  onfrALTlem3VD  45623