Theorem frege94

Description: Looking one past a pair related by transitive closure of a relation. Proposition 94 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege94.x	$$⊢X\in U$$
	frege94.z	$$⊢Z\in V$$
	frege94.r	$$⊢R\in W$$
Assertion	frege94	$$⊢\left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to \forall f\left(\forall w\left(XRw\to w\in f\right)\to \left(Rhereditaryf\to Z\in f\right)\right)\right)\right)\to \left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to X\mathrm{t+}\left(R\right)Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege94.x	$$⊢X\in U$$
2		frege94.z	$$⊢Z\in V$$
3		frege94.r	$$⊢R\in W$$
4	1 2 3	frege93	$$⊢\forall f\left(\forall w\left(XRw\to w\in f\right)\to \left(Rhereditaryf\to Z\in f\right)\right)\to X\mathrm{t+}\left(R\right)Z$$
5		frege7	$$⊢\left(\forall f\left(\forall w\left(XRw\to w\in f\right)\to \left(Rhereditaryf\to Z\in f\right)\right)\to X\mathrm{t+}\left(R\right)Z\right)\to \left(\left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to \forall f\left(\forall w\left(XRw\to w\in f\right)\to \left(Rhereditaryf\to Z\in f\right)\right)\right)\right)\to \left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to X\mathrm{t+}\left(R\right)Z\right)\right)\right)$$
6	4 5	ax-mp	$$⊢\left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to \forall f\left(\forall w\left(XRw\to w\in f\right)\to \left(Rhereditaryf\to Z\in f\right)\right)\right)\right)\to \left(YRZ\to \left(X\mathrm{t+}\left(R\right)Y\to X\mathrm{t+}\left(R\right)Z\right)\right)$$