Theorem frege97d

Description: If A contains all elements after those in U in the transitive closure of R , then the image under R of A is a subclass of A . Similar to Proposition 97 of Frege1879 p. 71. Compare with frege97 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege97d.r	|- ( ph -> R e. _V )
	frege97d.a	|- ( ph -> A = ( ( t+ ` R ) " U ) )
Assertion	frege97d	|- ( ph -> ( R " A ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		frege97d.r	|- ( ph -> R e. _V )
2		frege97d.a	|- ( ph -> A = ( ( t+ ` R ) " U ) )
3		trclfvlb	|- ( R e. _V -> R C_ ( t+ ` R ) )
4		coss1	|- ( R C_ ( t+ ` R ) -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
5	1 3 4	3syl	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
6		trclfvcotrg	|- ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )
7	5 6	sstrdi	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( t+ ` R ) )
8		imass1	|- ( ( R o. ( t+ ` R ) ) C_ ( t+ ` R ) -> ( ( R o. ( t+ ` R ) ) " U ) C_ ( ( t+ ` R ) " U ) )
9	7 8	syl	|- ( ph -> ( ( R o. ( t+ ` R ) ) " U ) C_ ( ( t+ ` R ) " U ) )
10	2	imaeq2d	|- ( ph -> ( R " A ) = ( R " ( ( t+ ` R ) " U ) ) )
11		imaco	|- ( ( R o. ( t+ ` R ) ) " U ) = ( R " ( ( t+ ` R ) " U ) )
12	10 11	eqtr4di	|- ( ph -> ( R " A ) = ( ( R o. ( t+ ` R ) ) " U ) )
13	9 12 2	3sstr4d	|- ( ph -> ( R " A ) C_ A )