Theorem wefr 5645

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

This proof depends on syntax axioms:   → wi 4   Or wor 5562   Fr wfr 5605   We wwe 5607

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 5610

This theorem is used by:  wefrc  5649  wereu  5651  wereu2  5652  tz6.26  6365  wfi  6367  wfisg  6369  wfis2fg  6371  ordfr  6392  wexp  8166  fnwe2lem3  8171  wfrfun  8366  wfrresex  8367  wfr2a  8368  wfr1  8369  wofib  9563  wemapso  9569  wemapso2lem  9570  cflim2  10365  fpwwe2lem11  10750  fpwwe2lem12  10751  fpwwe2  10752  ons2ind  28688  weiunwe  37434  welb  38861  onfrALTlem3  45716  onfrALTlem3VD  46058