Theorem wefr 5649

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

This proof depends on syntax axioms:   → wi 4   Or wor 5566   Fr wfr 5609   We wwe 5611

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 5614

This theorem is used by:  wefrc  5653  wereu  5655  wereu2  5656  tz6.26  6349  wfi  6351  wfisg  6353  wfis2fg  6355  ordfr  6376  wexp  8131  wfrfun  8325  wfrresex  8326  wfr2a  8327  wfr1  8328  wofib  9520  wemapso  9526  wemapso2lem  9527  cflim2  10268  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  ons2ind  28538  weiunwe  37075  welb  38473  fnwe2lem2  43879  onfrALTlem3  45354  onfrALTlem3VD  45696