Theorem wefr 5640

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

This proof depends on syntax axioms:   → wi 4   Or wor 5557   Fr wfr 5600   We wwe 5602

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 5605

This theorem is used by:  wefrc  5644  wereu  5646  wereu2  5647  tz6.26  6350  wfi  6352  wfisg  6354  wfis2fg  6356  ordfr  6377  wexp  8142  fnwe2lem3  8147  wfrfun  8341  wfrresex  8342  wfr2a  8343  wfr1  8344  wofib  9539  wemapso  9545  wemapso2lem  9546  cflim2  10341  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  ons2ind  28661  weiunwe  37257  welb  38671  onfrALTlem3  45527  onfrALTlem3VD  45869