Theorem wefr 5570

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

Syntax hints:   → wi 4   Or wor 5493   Fr wfr 5532   We wwe 5534

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 206  df-an 396  df-we 5537

This theorem is referenced by:  wefrc  5574  wereu  5576  wereu2  5577  tz6.26  6235  wfi  6238  wfisg  6241  wfis2fg  6244  ordfr  6266  wexp  7942  wfrlem14OLD  8124  wfrfun  8134  wfrresex  8135  wfr2a  8136  wfr1  8137  wofib  9234  wemapso  9240  wemapso2lem  9241  cflim2  9950  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  welb  35821  fnwe2lem2  40792  onfrALTlem3  42053  onfrALTlem3VD  42396