Theorem frege93

Description: Necessary condition for two elements to be related by the transitive closure. Proposition 93 of Frege1879 p. 70. (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	frege93	$$⊢\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\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		vex	$$⊢f\in \mathrm{V}$$
5	4	frege60c	$$⊢\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to \left(\underset{\dot{}}{[}f/f\underset{\dot{}}{]}Rhereditaryf\to \left(\underset{\dot{}}{[}f/f\underset{\dot{}}{]}\forall z\left(XRz\to z\in f\right)\to \underset{\dot{}}{[}f/f\underset{\dot{}}{]}Y\in f\right)\right)$$
6		sbcid	$$⊢\underset{\dot{}}{[}f/f\underset{\dot{}}{]}Rhereditaryf\leftrightarrow Rhereditaryf$$
7		sbcid	$$⊢\underset{\dot{}}{[}f/f\underset{\dot{}}{]}\forall z\left(XRz\to z\in f\right)\leftrightarrow \forall z\left(XRz\to z\in f\right)$$
8		sbcid	$$⊢\underset{\dot{}}{[}f/f\underset{\dot{}}{]}Y\in f\leftrightarrow Y\in f$$
9	7 8	imbi12i	$$⊢\left(\underset{\dot{}}{[}f/f\underset{\dot{}}{]}\forall z\left(XRz\to z\in f\right)\to \underset{\dot{}}{[}f/f\underset{\dot{}}{]}Y\in f\right)\leftrightarrow \left(\forall z\left(XRz\to z\in f\right)\to Y\in f\right)$$
10	5 6 9	3imtr3g	$$⊢\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to \left(Rhereditaryf\to \left(\forall z\left(XRz\to z\in f\right)\to Y\in f\right)\right)$$
11	10	axc4i	$$⊢\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to \forall f\left(Rhereditaryf\to \left(\forall z\left(XRz\to z\in f\right)\to Y\in f\right)\right)$$
12	1 2 3	frege90	$$⊢\left(\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to \forall f\left(Rhereditaryf\to \left(\forall z\left(XRz\to z\in f\right)\to Y\in f\right)\right)\right)\to \left(\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to X\mathrm{t+}\left(R\right)Y\right)$$
13	11 12	ax-mp	$$⊢\forall f\left(\forall z\left(XRz\to z\in f\right)\to \left(Rhereditaryf\to Y\in f\right)\right)\to X\mathrm{t+}\left(R\right)Y$$