Theorem zornn0

Description: Variant of Zorn's lemma zorn in which (/) , the union of the empty chain, is not required to be an element of A . (Contributed by Jeff Madsen, 5-Jan-2011)

	Ref	Expression
Hypothesis	zornn0.1	|- A e. _V
Assertion	zornn0	|- ( ( A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. 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		zornn0g	|- ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y )
5	3 4	mp3an1	|- ( ( A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y )