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	$$⊢\phi \to R\in \mathrm{V}$$
	frege97d.a	$$⊢\phi \to A=\mathrm{t+}\left(R\right)\left[U\right]$$
Assertion	frege97d	$$⊢\phi \to R\left[A\right]\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		frege97d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege97d.a	$$⊢\phi \to A=\mathrm{t+}\left(R\right)\left[U\right]$$
3		trclfvlb	$$⊢R\in \mathrm{V}\to R\subseteq \mathrm{t+}\left(R\right)$$
4		coss1	$$⊢R\subseteq \mathrm{t+}\left(R\right)\to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)$$
5	1 3 4	3syl	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)$$
6		trclfvcotrg	$$⊢\mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
7	5 6	sstrdi	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
8		imass1	$$⊢R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\to \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
9	7 8	syl	$$⊢\phi \to \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
10	2	imaeq2d	$$⊢\phi \to R\left[A\right]=R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]$$
11		imaco	$$⊢\left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]=R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]$$
12	10 11	eqtr4di	$$⊢\phi \to R\left[A\right]=\left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]$$
13	9 12 2	3sstr4d	$$⊢\phi \to R\left[A\right]\subseteq A$$