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 )