This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wefr

Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994)

		Ref	Expression
	Assertion	wefr	$⊢ R We A \to R Fr A$

Step	Hyp	Ref	Expression
1		df-we	$⊢ R We A \leftrightarrow (R Fr A \land R Or A)$
2	1	simplbi	$⊢ R We A \to R Fr A$