Metamath Proof Explorer

Theorem tz7.5

Description: A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of TakeutiZaring p. 36. (Contributed by NM, 18-Feb-2004) (Revised by David Abernethy, 16-Mar-2011)

		Ref	Expression
	Assertion	tz7.5	$⊢ (Ord A \land B \subseteq A \land B \neq \emptyset) \to \exists x \in B B \cap x = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ordwe	$⊢ Ord A \to E We A$
2		wefrc	$⊢ (E We A \land B \subseteq A \land B \neq \emptyset) \to \exists x \in B B \cap x = \emptyset$
3	1 2	syl3an1	$⊢ (Ord A \land B \subseteq A \land B \neq \emptyset) \to \exists x \in B B \cap x = \emptyset$