Theorem tc0

Description: The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015)

	Ref	Expression
Assertion	tc0	$$⊢\mathrm{TC}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\varnothing \subseteq \varnothing$$
2		tr0	$$⊢\mathrm{Tr}\varnothing$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		tcmin	$$⊢\varnothing \in \mathrm{V}\to \left(\left(\varnothing \subseteq \varnothing \wedge \mathrm{Tr}\varnothing \right)\to \mathrm{TC}\left(\varnothing \right)\subseteq \varnothing \right)$$
5	3 4	ax-mp	$$⊢\left(\varnothing \subseteq \varnothing \wedge \mathrm{Tr}\varnothing \right)\to \mathrm{TC}\left(\varnothing \right)\subseteq \varnothing$$
6	1 2 5	mp2an	$$⊢\mathrm{TC}\left(\varnothing \right)\subseteq \varnothing$$
7		0ss	$$⊢\varnothing \subseteq \mathrm{TC}\left(\varnothing \right)$$
8	6 7	eqssi	$$⊢\mathrm{TC}\left(\varnothing \right)=\varnothing$$