Theorem wefr 5624

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

Syntax hints:   → wi 4   Or wor 5541   Fr wfr 5584   We wwe 5586

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 207  df-an 396  df-we 5589

This theorem is referenced by:  wefrc  5628  wereu  5630  wereu2  5631  tz6.26  6315  wfi  6317  wfisg  6319  wfis2fg  6321  ordfr  6342  wexp  8084  wfrfun  8277  wfrresex  8278  wfr2a  8279  wfr1  8280  wofib  9464  wemapso  9470  wemapso2lem  9471  cflim2  10187  fpwwe2lem11  10566  fpwwe2lem12  10567  fpwwe2  10568  ons2ind  28288  weiunwe  36691  welb  38016  fnwe2lem2  43437  onfrALTlem3  44929  onfrALTlem3VD  45271