This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ 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 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )