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 =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )

Proof

Step	Hyp	Ref	Expression
1		issn	|- ( E. w e. A A. y e. A w = y -> E. z A = { z } )
2	1	olcd	|- ( E. w e. A A. y e. A w = y -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
3	2	a1d	|- ( E. w e. A A. y e. A w = y -> ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) ) )
4		df-ne	|- ( w =/= y <-> -. w = y )
5	4	rexbii	|- ( E. y e. A w =/= y <-> E. y e. A -. w = y )
6		rexnal	|- ( E. y e. A -. w = y <-> -. A. y e. A w = y )
7	5 6	bitri	|- ( E. y e. A w =/= y <-> -. A. y e. A w = y )
8	7	ralbii	|- ( A. w e. A E. y e. A w =/= y <-> A. w e. A -. A. y e. A w = y )
9		ralnex	|- ( A. w e. A -. A. y e. A w = y <-> -. E. w e. A A. y e. A w = y )
10	8 9	bitri	|- ( A. w e. A E. y e. A w =/= y <-> -. E. w e. A A. y e. A w = y )
11		neeq1	|- ( w = x -> ( w =/= y <-> x =/= y ) )
12	11	rexbidv	|- ( w = x -> ( E. y e. A w =/= y <-> E. y e. A x =/= y ) )
13	12	rspccva	|- ( ( A. w e. A E. y e. A w =/= y /\ x e. A ) -> E. y e. A x =/= y )
14	13	reximdva0	|- ( ( A. w e. A E. y e. A w =/= y /\ A =/= (/) ) -> E. x e. A E. y e. A x =/= y )
15	14	orcd	|- ( ( A. w e. A E. y e. A w =/= y /\ A =/= (/) ) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
16	15	ex	|- ( A. w e. A E. y e. A w =/= y -> ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) ) )
17	10 16	sylbir	|- ( -. E. w e. A A. y e. A w = y -> ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) ) )
18	3 17	pm2.61i	|- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )