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

Metamath Proof Explorer

Theorem tcsni

Description: The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

Ref Expression
Hypothesis tc2.1 
|- A e. _V
Assertion tcsni 
|- ( TC ` { A } ) = ( ( TC ` A ) u. { A } )

Proof

Step Hyp Ref Expression
1 tc2.1 
 |-  A e. _V
2 1 snss 
 |-  ( A e. x <-> { A } C_ x )
3 2 anbi1i 
 |-  ( ( A e. x /\ Tr x ) <-> ( { A } C_ x /\ Tr x ) )
4 3 abbii 
 |-  { x | ( A e. x /\ Tr x ) } = { x | ( { A } C_ x /\ Tr x ) }
5 4 inteqi 
 |-  |^| { x | ( A e. x /\ Tr x ) } = |^| { x | ( { A } C_ x /\ Tr x ) }
6 1 tc2 
 |-  ( ( TC ` A ) u. { A } ) = |^| { x | ( A e. x /\ Tr x ) }
7 snex 
 |-  { A } e. _V
8 tcvalg 
 |-  ( { A } e. _V -> ( TC ` { A } ) = |^| { x | ( { A } C_ x /\ Tr x ) } )
9 7 8 ax-mp 
 |-  ( TC ` { A } ) = |^| { x | ( { A } C_ x /\ Tr x ) }
10 5 6 9 3eqtr4ri 
 |-  ( TC ` { A } ) = ( ( TC ` A ) u. { A } )