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

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) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 12-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 df1o2 
 |-  1o = { (/) }
2 1 breq2i 
 |-  ( A ~<_ 1o <-> A ~<_ { (/) } )
3 brdomi 
 |-  ( A ~<_ { (/) } -> E. f f : A -1-1-> { (/) } )
4 f1cdmsn 
 |-  ( ( f : A -1-1-> { (/) } /\ A =/= (/) ) -> E. x A = { x } )
5 vex 
 |-  x e. _V
6 5 ensn1 
 |-  { x } ~~ 1o
7 breq1 
 |-  ( A = { x } -> ( A ~~ 1o <-> { x } ~~ 1o ) )
8 6 7 mpbiri 
 |-  ( A = { x } -> A ~~ 1o )
9 8 exlimiv 
 |-  ( E. x A = { x } -> A ~~ 1o )
10 4 9 syl 
 |-  ( ( f : A -1-1-> { (/) } /\ A =/= (/) ) -> A ~~ 1o )
11 10 expcom 
 |-  ( A =/= (/) -> ( f : A -1-1-> { (/) } -> A ~~ 1o ) )
12 11 exlimdv 
 |-  ( A =/= (/) -> ( E. f f : A -1-1-> { (/) } -> A ~~ 1o ) )
13 3 12 syl5 
 |-  ( A =/= (/) -> ( A ~<_ { (/) } -> A ~~ 1o ) )
14 2 13 biimtrid 
 |-  ( A =/= (/) -> ( A ~<_ 1o -> A ~~ 1o ) )
15 iman 
 |-  ( ( A ~<_ 1o -> A ~~ 1o ) <-> -. ( A ~<_ 1o /\ -. A ~~ 1o ) )
16 14 15 sylib 
 |-  ( A =/= (/) -> -. ( A ~<_ 1o /\ -. A ~~ 1o ) )
17 brsdom 
 |-  ( A ~< 1o <-> ( A ~<_ 1o /\ -. A ~~ 1o ) )
18 16 17 sylnibr 
 |-  ( A =/= (/) -> -. A ~< 1o )
19 18 necon4ai 
 |-  ( A ~< 1o -> A = (/) )
20 1n0 
 |-  1o =/= (/)
21 1oex 
 |-  1o e. _V
22 21 0sdom 
 |-  ( (/) ~< 1o <-> 1o =/= (/) )
23 20 22 mpbir 
 |-  (/) ~< 1o
24 breq1 
 |-  ( A = (/) -> ( A ~< 1o <-> (/) ~< 1o ) )
25 23 24 mpbiri 
 |-  ( A = (/) -> A ~< 1o )
26 19 25 impbii 
 |-  ( A ~< 1o <-> A = (/) )