Theorem zornn0

Description: Variant of Zorn's lemma zorn in which (/) , the union of the empty chain, is not required to be an element of A . (Contributed by Jeff Madsen, 5-Jan-2011)

	Ref	Expression
Hypothesis	zornn0.1	$$⊢A\in \mathrm{V}$$
Assertion	zornn0	$$⊢\left(A\ne \varnothing \wedge \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \wedge [\subset ]\mathrm{Or}z\right)\to \bigcup z\in A\right)\right)\to \exists x\in A\forall y\in A\neg x\subset y$$

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	$$⊢A\in \mathrm{V}$$
2		numth3	$$⊢A\in \mathrm{V}\to A\in \mathrm{dom}\mathrm{card}$$
3	1 2	ax-mp	$$⊢A\in \mathrm{dom}\mathrm{card}$$
4		zornn0g	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge A\ne \varnothing \wedge \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \wedge [\subset ]\mathrm{Or}z\right)\to \bigcup z\in A\right)\right)\to \exists x\in A\forall y\in A\neg x\subset y$$
5	3 4	mp3an1	$$⊢\left(A\ne \varnothing \wedge \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \wedge [\subset ]\mathrm{Or}z\right)\to \bigcup z\in A\right)\right)\to \exists x\in A\forall y\in A\neg x\subset y$$