Metamath Proof Explorer

Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion sdom1 
|- ( A ~< 1o <-> A = (/) )

Proof

Step Hyp Ref Expression
1 domnsym 
 |-  ( 1o ~<_ A -> -. A ~< 1o )
2 1 con2i 
 |-  ( A ~< 1o -> -. 1o ~<_ A )
3 0sdom1dom 
 |-  ( (/) ~< A <-> 1o ~<_ A )
4 2 3 sylnibr 
 |-  ( A ~< 1o -> -. (/) ~< A )
5 relsdom 
 |-  Rel ~<
6 5 brrelex1i 
 |-  ( A ~< 1o -> A e. _V )
7 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
8 7 necon2bbid 
 |-  ( A e. _V -> ( A = (/) <-> -. (/) ~< A ) )
9 6 8 syl 
 |-  ( A ~< 1o -> ( A = (/) <-> -. (/) ~< A ) )
10 4 9 mpbird 
 |-  ( A ~< 1o -> A = (/) )
11 1n0 
 |-  1o =/= (/)
12 1oex 
 |-  1o e. _V
13 12 0sdom 
 |-  ( (/) ~< 1o <-> 1o =/= (/) )
14 11 13 mpbir 
 |-  (/) ~< 1o
15 breq1 
 |-  ( A = (/) -> ( A ~< 1o <-> (/) ~< 1o ) )
16 14 15 mpbiri 
 |-  ( A = (/) -> A ~< 1o )
17 10 16 impbii 
 |-  ( A ~< 1o <-> A = (/) )