Theorem cnvsn0

Description: The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	cnvsn0	$$⊢{\left\{\varnothing \right\}}^{-1}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}\left\{\varnothing \right\}=\mathrm{ran}{\left\{\varnothing \right\}}^{-1}$$
2		dmsn0	$$⊢\mathrm{dom}\left\{\varnothing \right\}=\varnothing$$
3	1 2	eqtr3i	$$⊢\mathrm{ran}{\left\{\varnothing \right\}}^{-1}=\varnothing$$
4		relcnv	$$⊢\mathrm{Rel}{\left\{\varnothing \right\}}^{-1}$$
5		relrn0	$$⊢\mathrm{Rel}{\left\{\varnothing \right\}}^{-1}\to \left({\left\{\varnothing \right\}}^{-1}=\varnothing \leftrightarrow \mathrm{ran}{\left\{\varnothing \right\}}^{-1}=\varnothing \right)$$
6	4 5	ax-mp	$$⊢{\left\{\varnothing \right\}}^{-1}=\varnothing \leftrightarrow \mathrm{ran}{\left\{\varnothing \right\}}^{-1}=\varnothing$$
7	3 6	mpbir	$$⊢{\left\{\varnothing \right\}}^{-1}=\varnothing$$