Theorem zorn2

Description: Zorn's Lemma of Monk1 p. 117. This theorem is equivalent to the Axiom of Choice and states that every partially ordered set A (with an ordering relation R ) in which every totally ordered subset has an upper bound, contains at least one maximal element. The main proof consists of lemmas zorn2lem1 through zorn2lem7 ; this final piece mainly changes bound variables to eliminate the hypotheses of zorn2lem7 . (Contributed by NM, 6-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypothesis	zornn0.1	⊢ 𝐴 ∈ V
Assertion	zorn2	⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	⊢ 𝐴 ∈ V
2		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3	1 2	ax-mp	⊢ 𝐴 ∈ dom card
4		zorn2g	⊢ ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )
5	3 4	mp3an1	⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )