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

Proof

Step	Hyp	Ref	Expression
1		frege109d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege109d.a	$$⊢\phi \to A=U\cup \mathrm{t+}\left(R\right)\left[U\right]$$
3		trclfvlb	$$⊢R\in \mathrm{V}\to R\subseteq \mathrm{t+}\left(R\right)$$
4		imass1	$$⊢R\subseteq \mathrm{t+}\left(R\right)\to R\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
5	1 3 4	3syl	$$⊢\phi \to R\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
6		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)$$
7	1 3 6	3syl	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)$$
8		trclfvcotrg	$$⊢\mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
9	7 8	sstrdi	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
10		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]$$
11	9 10	syl	$$⊢\phi \to \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
12	5 11	unssd	$$⊢\phi \to R\left[U\right]\cup \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]\subseteq \mathrm{t+}\left(R\right)\left[U\right]$$
13		ssun2	$$⊢\mathrm{t+}\left(R\right)\left[U\right]\subseteq U\cup \mathrm{t+}\left(R\right)\left[U\right]$$
14	12 13	sstrdi	$$⊢\phi \to R\left[U\right]\cup \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]\subseteq U\cup \mathrm{t+}\left(R\right)\left[U\right]$$
15	2	imaeq2d	$$⊢\phi \to R\left[A\right]=R\left[U\cup \mathrm{t+}\left(R\right)\left[U\right]\right]$$
16		imaundi	$$⊢R\left[U\cup \mathrm{t+}\left(R\right)\left[U\right]\right]=R\left[U\right]\cup R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]$$
17		imaco	$$⊢\left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]=R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]$$
18	17	eqcomi	$$⊢R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]=\left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]$$
19	18	uneq2i	$$⊢R\left[U\right]\cup R\left[\mathrm{t+}\left(R\right)\left[U\right]\right]=R\left[U\right]\cup \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]$$
20	16 19	eqtri	$$⊢R\left[U\cup \mathrm{t+}\left(R\right)\left[U\right]\right]=R\left[U\right]\cup \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]$$
21	15 20	eqtrdi	$$⊢\phi \to R\left[A\right]=R\left[U\right]\cup \left(R\circ \mathrm{t+}\left(R\right)\right)\left[U\right]$$
22	14 21 2	3sstr4d	$$⊢\phi \to R\left[A\right]\subseteq A$$