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\preccurlyeq \varnothing \leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		brdomi	$$⊢A\preccurlyeq \varnothing \to \exists ff:A\underset{1-1}{⟶}\varnothing$$
2		f1f	$$⊢f:A\underset{1-1}{⟶}\varnothing \to f:A⟶\varnothing$$
3		f00	$$⊢f:A⟶\varnothing \leftrightarrow \left(f=\varnothing \wedge A=\varnothing \right)$$
4	3	simprbi	$$⊢f:A⟶\varnothing \to A=\varnothing$$
5	2 4	syl	$$⊢f:A\underset{1-1}{⟶}\varnothing \to A=\varnothing$$
6	5	exlimiv	$$⊢\exists ff:A\underset{1-1}{⟶}\varnothing \to A=\varnothing$$
7	1 6	syl	$$⊢A\preccurlyeq \varnothing \to A=\varnothing$$
8		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
9		endom	$$⊢A\approx \varnothing \to A\preccurlyeq \varnothing$$
10	8 9	sylbir	$$⊢A=\varnothing \to A\preccurlyeq \varnothing$$
11	7 10	impbii	$$⊢A\preccurlyeq \varnothing \leftrightarrow A=\varnothing$$