Theorem frege81d

Description: If the image of U is a subset U , A is an element of U and B follows A in the transitive closure of R , then B is an element of U . Similar to Proposition 81 of Frege1879 p. 63. Compare with frege81 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege81d.r	$$⊢\phi \to R\in \mathrm{V}$$
	frege81d.a	$$⊢\phi \to A\in U$$
	frege81d.b	$$⊢\phi \to B\in \mathrm{V}$$
	frege81d.ab	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$
	frege81d.he	$$⊢\phi \to R\left[U\right]\subseteq U$$
Assertion	frege81d	$$⊢\phi \to B\in U$$

Proof

Step	Hyp	Ref	Expression
1		frege81d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege81d.a	$$⊢\phi \to A\in U$$
3		frege81d.b	$$⊢\phi \to B\in \mathrm{V}$$
4		frege81d.ab	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$
5		frege81d.he	$$⊢\phi \to R\left[U\right]\subseteq U$$
6	2	elexd	$$⊢\phi \to A\in \mathrm{V}$$
7	2	snssd	$$⊢\phi \to \left\{A\right\}\subseteq U$$
8		imass2	$$⊢\left\{A\right\}\subseteq U\to R\left[\left\{A\right\}\right]\subseteq R\left[U\right]$$
9	7 8	syl	$$⊢\phi \to R\left[\left\{A\right\}\right]\subseteq R\left[U\right]$$
10	9 5	sstrd	$$⊢\phi \to R\left[\left\{A\right\}\right]\subseteq U$$
11	1 6 3 4 5 10	frege77d	$$⊢\phi \to B\in U$$