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