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

Metamath Proof Explorer

Theorem fri

Description: A nonempty subset of an R -well-founded class has an R -minimal element (inference form). (Contributed by BJ, 16-Nov-2024) (Proof shortened by BJ, 19-Nov-2024)

		Ref	Expression
	Assertion	fri	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to R Fr A$
2		simprl	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to B \subseteq A$
3		simpll	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to B \in C$
4		simprr	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to B \neq \emptyset$
5	1 2 3 4	frd	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$