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	⊢ 𝐴 ∈ V
Assertion	zornn0	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		zornn0.1	⊢ 𝐴 ∈ V
2		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3	1 2	ax-mp	⊢ 𝐴 ∈ dom card
4		zornn0g	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
5	3 4	mp3an1	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )