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

Metamath Proof Explorer

Theorem mo0sn

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mo0sn 
|- ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ z x e. A
2 nfv 
 |-  F/ x z e. A
3 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
4 1 2 3 cbvmow 
 |-  ( E* x x e. A <-> E* z z e. A )
5 neq0 
 |-  ( -. A = (/) <-> E. z z e. A )
6 5 anbi1i 
 |-  ( ( -. A = (/) /\ E* z z e. A ) <-> ( E. z z e. A /\ E* z z e. A ) )
7 df-eu 
 |-  ( E! z z e. A <-> ( E. z z e. A /\ E* z z e. A ) )
8 eu6 
 |-  ( E! z z e. A <-> E. y A. z ( z e. A <-> z = y ) )
9 6 7 8 3bitr2i 
 |-  ( ( -. A = (/) /\ E* z z e. A ) <-> E. y A. z ( z e. A <-> z = y ) )
10 dfcleq 
 |-  ( A = { y } <-> A. z ( z e. A <-> z e. { y } ) )
11 velsn 
 |-  ( z e. { y } <-> z = y )
12 11 bibi2i 
 |-  ( ( z e. A <-> z e. { y } ) <-> ( z e. A <-> z = y ) )
13 12 albii 
 |-  ( A. z ( z e. A <-> z e. { y } ) <-> A. z ( z e. A <-> z = y ) )
14 10 13 sylbbr 
 |-  ( A. z ( z e. A <-> z = y ) -> A = { y } )
15 14 eximi 
 |-  ( E. y A. z ( z e. A <-> z = y ) -> E. y A = { y } )
16 9 15 sylbi 
 |-  ( ( -. A = (/) /\ E* z z e. A ) -> E. y A = { y } )
17 16 expcom 
 |-  ( E* z z e. A -> ( -. A = (/) -> E. y A = { y } ) )
18 17 orrd 
 |-  ( E* z z e. A -> ( A = (/) \/ E. y A = { y } ) )
19 mo0 
 |-  ( A = (/) -> E* z z e. A )
20 mosn 
 |-  ( A = { y } -> E* z z e. A )
21 20 exlimiv 
 |-  ( E. y A = { y } -> E* z z e. A )
22 19 21 jaoi 
 |-  ( ( A = (/) \/ E. y A = { y } ) -> E* z z e. A )
23 18 22 impbii 
 |-  ( E* z z e. A <-> ( A = (/) \/ E. y A = { y } ) )
24 4 23 bitri 
 |-  ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )