Theorem wefr 5611

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

Syntax hints:   → wi 4   Or wor 5528   Fr wfr 5571   We wwe 5573

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 398  df-we 5576

This theorem is referenced by:  wefrc  5615  wereu  5617  wereu2  5618  tz6.26  6302  wfi  6304  wfisg  6306  wfis2fg  6308  ordfr  6329  wexp  8074  wfrfun  8267  wfrresex  8268  wfr2a  8269  wfr1  8270  wofib  9454  wemapso  9460  wemapso2lem  9461  cflim2  10180  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwe2  10561  ons2ind  28289  weiunwe  36712  welb  38118  fnwe2lem2  43511  onfrALTlem3  45003  onfrALTlem3VD  45345