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	$$⊢\left(\mathrm{Ord}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in BB\cap x=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ordwe	$$⊢\mathrm{Ord}A\to \mathrm{E}\mathrm{We}A$$
2		wefrc	$$⊢\left(\mathrm{E}\mathrm{We}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in BB\cap x=\varnothing$$
3	1 2	syl3an1	$$⊢\left(\mathrm{Ord}A\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in BB\cap x=\varnothing$$