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 V$
	Assertion	zorn2	$⊢ (R Po A \land \forall w ((w \subseteq A \land R Or w) \to \exists x \in A \forall z \in w (z R x \lor z = x))) \to \exists x \in A \forall y \in A \neg x R y$

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	$⊢ A \in V$
2		numth3	$⊢ A \in V \to A \in dom card$
3	1 2	ax-mp	$⊢ A \in dom card$
4		zorn2g	$⊢ (A \in dom card \land R Po A \land \forall w ((w \subseteq A \land R Or w) \to \exists x \in A \forall z \in w (z R x \lor z = x))) \to \exists x \in A \forall y \in A \neg x R y$
5	3 4	mp3an1	$⊢ (R Po A \land \forall w ((w \subseteq A \land R Or w) \to \exists x \in A \forall z \in w (z R x \lor z = x))) \to \exists x \in A \forall y \in A \neg x R y$

Metamath Proof Explorer

Theorem zorn2

Proof