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
|- A e. _V
Assertion zorn2
|- ( ( R Po A /\ A. w ( ( w C_ A /\ R Or w ) -> E. x e. A A. z e. w ( z R x \/ z = x ) ) ) -> E. x e. A A. y e. A -. x R y )

Proof

Step Hyp Ref Expression
1 zornn0.1
 |-  A e. _V
2 numth3
 |-  ( A e. _V -> A e. dom card )
3 1 2 ax-mp
 |-  A e. dom card
4 zorn2g
 |-  ( ( A e. dom card /\ R Po A /\ A. w ( ( w C_ A /\ R Or w ) -> E. x e. A A. z e. w ( z R x \/ z = x ) ) ) -> E. x e. A A. y e. A -. x R y )
5 3 4 mp3an1
 |-  ( ( R Po A /\ A. w ( ( w C_ A /\ R Or w ) -> E. x e. A A. z e. w ( z R x \/ z = x ) ) ) -> E. x e. A A. y e. A -. x R y )