This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 V$
	Assertion	zorn	$⊢ \forall z ((z \subseteq A \land [\subset] Or z) \to ⋃ z \in A) \to \exists x \in A \forall y \in A \neg x \subset y$

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	$⊢ A \in V$
2		numth3	$⊢ A \in V \to A \in dom card$
3	1 2	ax-mp	$⊢ A \in dom card$
4		zorng	$⊢ (A \in dom card \land \forall z ((z \subseteq A \land [\subset] Or z) \to ⋃ z \in A)) \to \exists x \in A \forall y \in A \neg x \subset y$
5	3 4	mpan	$⊢ \forall z ((z \subseteq A \land [\subset] Or z) \to ⋃ z \in A) \to \exists x \in A \forall y \in A \neg x \subset y$