Theorem wefr 5539

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

Syntax hints:   → wi 4   Or wor 5467   Fr wfr 5505   We wwe 5507

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 5510

This theorem is referenced by:  wefrc  5543  wereu  5545  wereu2  5546  ordfr  6200  wexp  7818  wfrlem14  7962  wofib  9003  wemapso  9009  wemapso2lem  9010  cflim2  9679  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  welb  35005  fnwe2lem2  39644  onfrALTlem3  40871  onfrALTlem3VD  41214