Metamath Proof Explorer


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 )