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	⊢ 𝐴 ∈ V
	Assertion	zorn	⊢ ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	⊢ 𝐴 ∈ V
2		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3	1 2	ax-mp	⊢ 𝐴 ∈ dom card
4		zorng	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
5	3 4	mpan	⊢ ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )