Theorem supp0

Description: The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Assertion	supp0	$$⊢Z\in W\to \varnothing \mathrm{supp}Z=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		suppval	$$⊢\left(\varnothing \in \mathrm{V}\wedge Z\in W\right)\to \varnothing \mathrm{supp}Z=\left\{i\in \mathrm{dom}\varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}$$
3	1 2	mpan	$$⊢Z\in W\to \varnothing \mathrm{supp}Z=\left\{i\in \mathrm{dom}\varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}$$
4		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
5		rabeq	$$⊢\mathrm{dom}\varnothing =\varnothing \to \left\{i\in \mathrm{dom}\varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}=\left\{i\in \varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}$$
6	4 5	mp1i	$$⊢Z\in W\to \left\{i\in \mathrm{dom}\varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}=\left\{i\in \varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}$$
7		rab0	$$⊢\left\{i\in \varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}=\varnothing$$
8	7	a1i	$$⊢Z\in W\to \left\{i\in \varnothing |\varnothing \left[\left\{i\right\}\right]\ne \left\{Z\right\}\right\}=\varnothing$$
9	3 6 8	3eqtrd	$$⊢Z\in W\to \varnothing \mathrm{supp}Z=\varnothing$$