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\in \mathrm{V}$$
Assertion	zorn2	$$⊢\left(R\mathrm{Po}A\wedge \forall w\left(\left(w\subseteq A\wedge R\mathrm{Or}w\right)\to \exists x\in A\forall z\in w\left(zRx\vee z=x\right)\right)\right)\to \exists x\in A\forall y\in A\neg xRy$$

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	$$⊢A\in \mathrm{V}$$
2		numth3	$$⊢A\in \mathrm{V}\to A\in \mathrm{dom}\mathrm{card}$$
3	1 2	ax-mp	$$⊢A\in \mathrm{dom}\mathrm{card}$$
4		zorn2g	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge R\mathrm{Po}A\wedge \forall w\left(\left(w\subseteq A\wedge R\mathrm{Or}w\right)\to \exists x\in A\forall z\in w\left(zRx\vee z=x\right)\right)\right)\to \exists x\in A\forall y\in A\neg xRy$$
5	3 4	mp3an1	$$⊢\left(R\mathrm{Po}A\wedge \forall w\left(\left(w\subseteq A\wedge R\mathrm{Or}w\right)\to \exists x\in A\forall z\in w\left(zRx\vee z=x\right)\right)\right)\to \exists x\in A\forall y\in A\neg xRy$$