Theorem frege109d

Description: If A contains all elements of U and 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 109 of Frege1879 p. 74. Compare with frege109 . (Contributed by RP, 15-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		frege109d.r	|- ( ph -> R e. _V )
2		frege109d.a	|- ( ph -> A = ( U u. ( ( t+ ` R ) " U ) ) )
3		trclfvlb	|- ( R e. _V -> R C_ ( t+ ` R ) )
4		imass1	|- ( R C_ ( t+ ` R ) -> ( R " U ) C_ ( ( t+ ` R ) " U ) )
5	1 3 4	3syl	|- ( ph -> ( R " U ) C_ ( ( t+ ` R ) " U ) )
6		coss1	|- ( R C_ ( t+ ` R ) -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
7	1 3 6	3syl	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
8		trclfvcotrg	|- ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )
9	7 8	sstrdi	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( t+ ` R ) )
10		imass1	|- ( ( R o. ( t+ ` R ) ) C_ ( t+ ` R ) -> ( ( R o. ( t+ ` R ) ) " U ) C_ ( ( t+ ` R ) " U ) )
11	9 10	syl	|- ( ph -> ( ( R o. ( t+ ` R ) ) " U ) C_ ( ( t+ ` R ) " U ) )
12	5 11	unssd	|- ( ph -> ( ( R " U ) u. ( ( R o. ( t+ ` R ) ) " U ) ) C_ ( ( t+ ` R ) " U ) )
13		ssun2	|- ( ( t+ ` R ) " U ) C_ ( U u. ( ( t+ ` R ) " U ) )
14	12 13	sstrdi	|- ( ph -> ( ( R " U ) u. ( ( R o. ( t+ ` R ) ) " U ) ) C_ ( U u. ( ( t+ ` R ) " U ) ) )
15	2	imaeq2d	|- ( ph -> ( R " A ) = ( R " ( U u. ( ( t+ ` R ) " U ) ) ) )
16		imaundi	|- ( R " ( U u. ( ( t+ ` R ) " U ) ) ) = ( ( R " U ) u. ( R " ( ( t+ ` R ) " U ) ) )
17		imaco	|- ( ( R o. ( t+ ` R ) ) " U ) = ( R " ( ( t+ ` R ) " U ) )
18	17	eqcomi	|- ( R " ( ( t+ ` R ) " U ) ) = ( ( R o. ( t+ ` R ) ) " U )
19	18	uneq2i	|- ( ( R " U ) u. ( R " ( ( t+ ` R ) " U ) ) ) = ( ( R " U ) u. ( ( R o. ( t+ ` R ) ) " U ) )
20	16 19	eqtri	|- ( R " ( U u. ( ( t+ ` R ) " U ) ) ) = ( ( R " U ) u. ( ( R o. ( t+ ` R ) ) " U ) )
21	15 20	eqtrdi	|- ( ph -> ( R " A ) = ( ( R " U ) u. ( ( R o. ( t+ ` R ) ) " U ) ) )
22	14 21 2	3sstr4d	|- ( ph -> ( R " A ) C_ A )