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