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 ) )