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

Metamath Proof Explorer

Theorem n0snor2el

Description: A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020)

Ref Expression
Assertion n0snor2el ⊢ A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z

Proof

Step Hyp Ref Expression
1 issn ⊢ ∃ w ∈ A ∀ y ∈ A w = y → ∃ z A = z
2 1 olcd ⊢ ∃ w ∈ A ∀ y ∈ A w = y → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z
3 2 a1d ⊢ ∃ w ∈ A ∀ y ∈ A w = y → A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z
4 df-ne ⊢ w ≠ y ↔ ¬ w = y
5 4 rexbii ⊢ ∃ y ∈ A w ≠ y ↔ ∃ y ∈ A ¬ w = y
6 rexnal ⊢ ∃ y ∈ A ¬ w = y ↔ ¬ ∀ y ∈ A w = y
7 5 6 bitri ⊢ ∃ y ∈ A w ≠ y ↔ ¬ ∀ y ∈ A w = y
8 7 ralbii ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y ↔ ∀ w ∈ A ¬ ∀ y ∈ A w = y
9 ralnex ⊢ ∀ w ∈ A ¬ ∀ y ∈ A w = y ↔ ¬ ∃ w ∈ A ∀ y ∈ A w = y
10 8 9 bitri ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y ↔ ¬ ∃ w ∈ A ∀ y ∈ A w = y
11 neeq1 ⊢ w = x → w ≠ y ↔ x ≠ y
12 11 rexbidv ⊢ w = x → ∃ y ∈ A w ≠ y ↔ ∃ y ∈ A x ≠ y
13 12 rspccva ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y ∧ x ∈ A → ∃ y ∈ A x ≠ y
14 13 reximdva0 ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y ∧ A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y
15 14 orcd ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y ∧ A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z
16 15 ex ⊢ ∀ w ∈ A ∃ y ∈ A w ≠ y → A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z
17 10 16 sylbir ⊢ ¬ ∃ w ∈ A ∀ y ∈ A w = y → A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z
18 3 17 pm2.61i ⊢ A ≠ ∅ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∨ ∃ z A = z