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 
 |-  (/) C_ (/)
2 tr0 
 |-  Tr (/)
3 0ex 
 |-  (/) e. _V
4 tcmin 
 |-  ( (/) e. _V -> ( ( (/) C_ (/) /\ Tr (/) ) -> ( TC ` (/) ) C_ (/) ) )
5 3 4 ax-mp 
 |-  ( ( (/) C_ (/) /\ Tr (/) ) -> ( TC ` (/) ) C_ (/) )
6 1 2 5 mp2an 
 |-  ( TC ` (/) ) C_ (/)
7 0ss 
 |-  (/) C_ ( TC ` (/) )
8 6 7 eqssi 
 |-  ( TC ` (/) ) = (/)