This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ ∅ = ∅