Theorem frege87d

Description: If the images of both { A } and U are subsets of U and C follows A in the transitive closure of R and B follows C in R , then B is an element of U . Similar to Proposition 87 of Frege1879 p. 66. Compare with frege87 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege87d.r	$$⊢\phi \to R\in \mathrm{V}$$
	frege87d.a	$$⊢\phi \to A\in \mathrm{V}$$
	frege87d.b	$$⊢\phi \to B\in \mathrm{V}$$
	frege87d.c	$$⊢\phi \to C\in \mathrm{V}$$
	frege87d.ac	$$⊢\phi \to A\mathrm{t+}\left(R\right)C$$
	frege87d.cb	$$⊢\phi \to CRB$$
	frege87d.ss	$$⊢\phi \to R\left[\left\{A\right\}\right]\subseteq U$$
	frege87d.he	$$⊢\phi \to R\left[U\right]\subseteq U$$
Assertion	frege87d	$$⊢\phi \to B\in U$$

Proof

Step	Hyp	Ref	Expression
1		frege87d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege87d.a	$$⊢\phi \to A\in \mathrm{V}$$
3		frege87d.b	$$⊢\phi \to B\in \mathrm{V}$$
4		frege87d.c	$$⊢\phi \to C\in \mathrm{V}$$
5		frege87d.ac	$$⊢\phi \to A\mathrm{t+}\left(R\right)C$$
6		frege87d.cb	$$⊢\phi \to CRB$$
7		frege87d.ss	$$⊢\phi \to R\left[\left\{A\right\}\right]\subseteq U$$
8		frege87d.he	$$⊢\phi \to R\left[U\right]\subseteq U$$
9	1 2 3 4 5 6	frege96d	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$
10	1 2 3 9 8 7	frege77d	$$⊢\phi \to B\in U$$