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 =/= (/) -> ( 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 } ) )