Theorem tc0

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

	Ref	Expression
Assertion	tc0	⊢ ( TC ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ∅ ⊆ ∅
2		tr0	⊢ Tr ∅
3		0ex	⊢ ∅ ∈ V
4		tcmin	⊢ ( ∅ ∈ V → ( ( ∅ ⊆ ∅ ∧ Tr ∅ ) → ( TC ‘ ∅ ) ⊆ ∅ ) )
5	3 4	ax-mp	⊢ ( ( ∅ ⊆ ∅ ∧ Tr ∅ ) → ( TC ‘ ∅ ) ⊆ ∅ )
6	1 2 5	mp2an	⊢ ( TC ‘ ∅ ) ⊆ ∅
7		0ss	⊢ ∅ ⊆ ( TC ‘ ∅ )
8	6 7	eqssi	⊢ ( TC ‘ ∅ ) = ∅