Theorem dom0

Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	dom0	|- ( A ~<_ (/) <-> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		brdomi	|- ( A ~<_ (/) -> E. f f : A -1-1-> (/) )
2		f1f	|- ( f : A -1-1-> (/) -> f : A --> (/) )
3		f00	|- ( f : A --> (/) <-> ( f = (/) /\ A = (/) ) )
4	3	simprbi	|- ( f : A --> (/) -> A = (/) )
5	2 4	syl	|- ( f : A -1-1-> (/) -> A = (/) )
6	5	exlimiv	|- ( E. f f : A -1-1-> (/) -> A = (/) )
7	1 6	syl	|- ( A ~<_ (/) -> A = (/) )
8		en0	|- ( A ~~ (/) <-> A = (/) )
9		endom	|- ( A ~~ (/) -> A ~<_ (/) )
10	8 9	sylbir	|- ( A = (/) -> A ~<_ (/) )
11	7 10	impbii	|- ( A ~<_ (/) <-> A = (/) )