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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege97d.a	⊢ ( 𝜑 → 𝐴 = ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
Assertion	frege97d	⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		frege97d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege97d.a	⊢ ( 𝜑 → 𝐴 = ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
3		trclfvlb	⊢ ( 𝑅 ∈ V → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
4		coss1	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
5	1 3 4	3syl	⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
6		trclfvcotrg	⊢ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 )
7	5 6	sstrdi	⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
8		imass1	⊢ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) → ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
9	7 8	syl	⊢ ( 𝜑 → ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
10	2	imaeq2d	⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) = ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) )
11		imaco	⊢ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) = ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
12	10 11	eqtr4di	⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) = ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) )
13	9 12 2	3sstr4d	⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )