Theorem frege91

Description: Every result of an application of a procedure R to an object X follows that X in the R -sequence. Proposition 91 of Frege1879 p. 68. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege91.x	$$⊢X\in U$$
	frege91.y	$$⊢Y\in V$$
	frege91.r	$$⊢R\in W$$
Assertion	frege91	$$⊢XRY\to X\mathrm{t+}\left(R\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		frege91.x	$$⊢X\in U$$
2		frege91.y	$$⊢Y\in V$$
3		frege91.r	$$⊢R\in W$$
4	2	frege63c	$$⊢\underset{\dot{}}{[}Y/a\underset{\dot{}}{]}XRa\to \left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}Y/a\underset{\dot{}}{]}a\in f\right)\right)$$
5		sbcbr2g	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/a\underset{\dot{}}{]}XRa\leftrightarrow XR⦋Y/a⦌a\right)$$
6		csbvarg	$$⊢Y\in V\to ⦋Y/a⦌a=Y$$
7	6	breq2d	$$⊢Y\in V\to \left(XR⦋Y/a⦌a\leftrightarrow XRY\right)$$
8	5 7	bitrd	$$⊢Y\in V\to \left(\underset{\dot{}}{[}Y/a\underset{\dot{}}{]}XRa\leftrightarrow XRY\right)$$
9	2 8	ax-mp	$$⊢\underset{\dot{}}{[}Y/a\underset{\dot{}}{]}XRa\leftrightarrow XRY$$
10		sbcel1v	$$⊢\underset{\dot{}}{[}Y/a\underset{\dot{}}{]}a\in f\leftrightarrow Y\in f$$
11	10	imbi2i	$$⊢\left(\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}Y/a\underset{\dot{}}{]}a\in f\right)\leftrightarrow \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)$$
12	11	imbi2i	$$⊢\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}Y/a\underset{\dot{}}{]}a\in f\right)\right)\leftrightarrow \left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)$$
13	4 9 12	3imtr3i	$$⊢XRY\to \left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)$$
14	13	alrimiv	$$⊢XRY\to \forall f\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)$$
15	1 2 3	frege90	$$⊢\left(XRY\to \forall f\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\right)\to \left(XRY\to X\mathrm{t+}\left(R\right)Y\right)$$
16	14 15	ax-mp	$$⊢XRY\to X\mathrm{t+}\left(R\right)Y$$