Theorem trclfvss

Description: The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020)

	Ref	Expression
Assertion	trclfvss	|- ( ( R e. V /\ S e. W /\ R C_ S ) -> ( t+ ` R ) C_ ( t+ ` S ) )

Proof

Step	Hyp	Ref	Expression
1		trclsslem	|- ( R C_ S -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
2	1	3ad2ant3	|- ( ( R e. V /\ S e. W /\ R C_ S ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
3		trclfv	|- ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
4	3	3ad2ant1	|- ( ( R e. V /\ S e. W /\ R C_ S ) -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
5		trclfv	|- ( S e. W -> ( t+ ` S ) = |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
6	5	3ad2ant2	|- ( ( R e. V /\ S e. W /\ R C_ S ) -> ( t+ ` S ) = |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
7	2 4 6	3sstr4d	|- ( ( R e. V /\ S e. W /\ R C_ S ) -> ( t+ ` R ) C_ ( t+ ` S ) )