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

Metamath Proof Explorer

Theorem tcss

Description: The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Hypothesis tc2.1 
|- A e. _V
Assertion tcss 
|- ( B C_ A -> ( TC ` B ) C_ ( TC ` A ) )

Proof

Step Hyp Ref Expression
1 tc2.1 
 |-  A e. _V
2 1 ssex 
 |-  ( B C_ A -> B e. _V )
3 tcvalg 
 |-  ( B e. _V -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } )
4 2 3 syl 
 |-  ( B C_ A -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } )
5 sstr2 
 |-  ( B C_ A -> ( A C_ x -> B C_ x ) )
6 5 anim1d 
 |-  ( B C_ A -> ( ( A C_ x /\ Tr x ) -> ( B C_ x /\ Tr x ) ) )
7 6 ss2abdv 
 |-  ( B C_ A -> { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } )
8 intss 
 |-  ( { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } )
9 7 8 syl 
 |-  ( B C_ A -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } )
10 tcvalg 
 |-  ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
11 1 10 ax-mp 
 |-  ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) }
12 9 11 sseqtrrdi 
 |-  ( B C_ A -> |^| { x | ( B C_ x /\ Tr x ) } C_ ( TC ` A ) )
13 4 12 eqsstrd 
 |-  ( B C_ A -> ( TC ` B ) C_ ( TC ` A ) )