Metamath Proof Explorer


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 φ R V
frege97d.a φ A = t+ R U
Assertion frege97d φ R A A

Proof

Step Hyp Ref Expression
1 frege97d.r φ R V
2 frege97d.a φ A = t+ R U
3 trclfvlb R V R t+ R
4 coss1 R t+ R R t+ R t+ R t+ R
5 1 3 4 3syl φ R t+ R t+ R t+ R
6 trclfvcotrg t+ R t+ R t+ R
7 5 6 sstrdi φ R t+ R t+ R
8 imass1 R t+ R t+ R R t+ R U t+ R U
9 7 8 syl φ R t+ R U t+ R U
10 2 imaeq2d φ R A = R t+ R U
11 imaco R t+ R U = R t+ R U
12 10 11 eqtr4di φ R A = R t+ R U
13 9 12 2 3sstr4d φ R A A