tz6.26

Description: All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Proof shortened by Scott Fenton, 17-Nov-2024)

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		wefr	$⊢ R We A \to R Fr A$
2	1	adantr	$⊢ (R We A \land R Se A) \to R Fr A$
3		weso	$⊢ R We A \to R Or A$
4		sopo	$⊢ R Or A \to R Po A$
5	3 4	syl	$⊢ R We A \to R Po A$
6	5	adantr	$⊢ (R We A \land R Se A) \to R Po A$
7		simpr	$⊢ (R We A \land R Se A) \to R Se A$
8	2 6 7	3jca	$⊢ (R We A \land R Se A) \to (R Fr A \land R Po A \land R Se A)$
9		frpomin2	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists y \in B Pred (R, B, y) = \emptyset$
10	8 9	sylan	$⊢ ((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$

Metamath Proof Explorer

Theorem tz6.26

Proof