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 ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑧 𝐴 = { 𝑧 } ) )

Proof

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