Theorem tcel

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

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

Proof

Step	Hyp	Ref	Expression
1		tc2.1	|- A e. _V
2		tcvalg	|- ( B e. A -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } )
3		ssel	|- ( A C_ x -> ( B e. A -> B e. x ) )
4		trss	|- ( Tr x -> ( B e. x -> B C_ x ) )
5	4	com12	|- ( B e. x -> ( Tr x -> B C_ x ) )
6	3 5	syl6com	|- ( B e. A -> ( A C_ x -> ( Tr x -> B C_ x ) ) )
7	6	impd	|- ( B e. A -> ( ( A C_ x /\ Tr x ) -> B C_ x ) )
8		simpr	|- ( ( A C_ x /\ Tr x ) -> Tr x )
9	7 8	jca2	|- ( B e. A -> ( ( A C_ x /\ Tr x ) -> ( B C_ x /\ Tr x ) ) )
10	9	ss2abdv	|- ( B e. A -> { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } )
11		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 ) } )
12	10 11	syl	|- ( B e. A -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } )
13		tcvalg	|- ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
14	1 13	ax-mp	|- ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) }
15	12 14	sseqtrrdi	|- ( B e. A -> |^| { x | ( B C_ x /\ Tr x ) } C_ ( TC ` A ) )
16	2 15	eqsstrd	|- ( B e. A -> ( TC ` B ) C_ ( TC ` A ) )