Theorem wefr 5547

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

Syntax hints:   → wi 4   Or wor 5475   Fr wfr 5513   We wwe 5515

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 209  df-an 399  df-we 5518

This theorem is referenced by:  wefrc  5551  wereu  5553  wereu2  5554  ordfr  6208  wexp  7826  wfrlem14  7970  wofib  9011  wemapso  9017  wemapso2lem  9018  cflim2  9687  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  welb  35013  fnwe2lem2  39658  onfrALTlem3  40885  onfrALTlem3VD  41228