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