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

Metamath Proof Explorer

Theorem tz6.26i

Description: All nonempty subclasses of a class having a well-ordered set-like relation R have R-minimal elements. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 14-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	tz6.26i.1	$⊢ R We A$
	tz6.26i.2	$⊢ R Se A$
Assertion	tz6.26i	$⊢ (B \subseteq A \land B \neq \emptyset) \to \exists y \in B Pred (R, B, y) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		tz6.26i.1	$⊢ R We A$
2		tz6.26i.2	$⊢ R Se A$
3		tz6.26	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists y \in B Pred (R, B, y) = \emptyset$
4	1 2 3	mpanl12	$⊢ (B \subseteq A \land B \neq \emptyset) \to \exists y \in B Pred (R, B, y) = \emptyset$