Theorem zorn

Description: Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. This theorem is equivalent to the Axiom of Choice. Theorem 6M of Enderton p. 151. See zorn2 for a version with general partial orderings. (Contributed by NM, 12-Aug-2004)

	Ref	Expression
Hypothesis	zornn0.1	$$⊢A\in \mathrm{V}$$
Assertion	zorn	$$⊢\forall z\left(\left(z\subseteq A\wedge [\subset ]\mathrm{Or}z\right)\to \bigcup z\in A\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		zorng	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \forall z\left(\left(z\subseteq A\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	mpan	$$⊢\forall z\left(\left(z\subseteq A\wedge [\subset ]\mathrm{Or}z\right)\to \bigcup z\in A\right)\to \exists x\in A\forall y\in A\neg x\subset y$$