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

Metamath Proof Explorer

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 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )