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 AV
Assertion zorn2 RPoAwwAROrwxAzwzRxz=xxAyA¬xRy

Proof

Step Hyp Ref Expression
1 zornn0.1 AV
2 numth3 AVAdomcard
3 1 2 ax-mp Adomcard
4 zorn2g AdomcardRPoAwwAROrwxAzwzRxz=xxAyA¬xRy
5 3 4 mp3an1 RPoAwwAROrwxAzwzRxz=xxAyA¬xRy