Theorem frege77

Description: If Y follows X in the R -sequence, if property A is hereditary in the R -sequence, and if every result of an application of the procedure R to X has the property A , then Y has property A . Proposition 77 of Frege1879 p. 62. (Contributed by RP, 29-Jun-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege77.x	$$⊢X\in U$$
	frege77.y	$$⊢Y\in V$$
	frege77.r	$$⊢R\in W$$
	frege77.a	$$⊢A\in B$$
Assertion	frege77	$$⊢X\mathrm{t+}\left(R\right)Y\to \left(RhereditaryA\to \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege77.x	$$⊢X\in U$$
2		frege77.y	$$⊢Y\in V$$
3		frege77.r	$$⊢R\in W$$
4		frege77.a	$$⊢A\in B$$
5	1 2 3	dffrege76	$$⊢\forall f\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow X\mathrm{t+}\left(R\right)Y$$
6	4	frege68c	$$⊢\left(\forall f\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow X\mathrm{t+}\left(R\right)Y\right)\to \left(X\mathrm{t+}\left(R\right)Y\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\right)$$
7		sbcimg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\right)$$
8	4 7	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)$$
9		sbcheg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\leftrightarrow ⦋A/f⦌Rhereditary⦋A/f⦌f\right)$$
10	4 9	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\leftrightarrow ⦋A/f⦌Rhereditary⦋A/f⦌f$$
11		csbconstg	$$⊢A\in B\to ⦋A/f⦌R=R$$
12	4 11	ax-mp	$$⊢⦋A/f⦌R=R$$
13		csbvarg	$$⊢A\in B\to ⦋A/f⦌f=A$$
14	4 13	ax-mp	$$⊢⦋A/f⦌f=A$$
15		heeq12	$$⊢\left(⦋A/f⦌R=R\wedge ⦋A/f⦌f=A\right)\to \left(⦋A/f⦌Rhereditary⦋A/f⦌f\leftrightarrow RhereditaryA\right)$$
16	12 14 15	mp2an	$$⊢⦋A/f⦌Rhereditary⦋A/f⦌f\leftrightarrow RhereditaryA$$
17	10 16	bitri	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\leftrightarrow RhereditaryA$$
18		sbcimg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}Y\in f\right)\right)$$
19	4 18	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}Y\in f\right)$$
20		sbcal	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\forall a\left(XRa\to a\in f\right)\leftrightarrow \forall a\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(XRa\to a\in f\right)$$
21		sbcimg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(XRa\to a\in f\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}XRa\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}a\in f\right)\right)$$
22	4 21	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(XRa\to a\in f\right)\leftrightarrow \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}XRa\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}a\in f\right)$$
23		sbcg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}XRa\leftrightarrow XRa\right)$$
24	4 23	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}XRa\leftrightarrow XRa$$
25		sbcel2gv	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}a\in f\leftrightarrow a\in A\right)$$
26	4 25	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}a\in f\leftrightarrow a\in A$$
27	24 26	imbi12i	$$⊢\left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}XRa\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}a\in f\right)\leftrightarrow \left(XRa\to a\in A\right)$$
28	22 27	bitri	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(XRa\to a\in f\right)\leftrightarrow \left(XRa\to a\in A\right)$$
29	28	albii	$$⊢\forall a\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(XRa\to a\in f\right)\leftrightarrow \forall a\left(XRa\to a\in A\right)$$
30	20 29	bitri	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\forall a\left(XRa\to a\in f\right)\leftrightarrow \forall a\left(XRa\to a\in A\right)$$
31		sbcel2gv	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Y\in f\leftrightarrow Y\in A\right)$$
32	4 31	ax-mp	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Y\in f\leftrightarrow Y\in A$$
33	30 32	imbi12i	$$⊢\left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\forall a\left(XRa\to a\in f\right)\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}Y\in f\right)\leftrightarrow \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)$$
34	19 33	bitri	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\leftrightarrow \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)$$
35	17 34	imbi12i	$$⊢\left(\underset{\dot{}}{[}A/f\underset{\dot{}}{]}Rhereditaryf\to \underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow \left(RhereditaryA\to \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)\right)$$
36	8 35	bitri	$$⊢\underset{\dot{}}{[}A/f\underset{\dot{}}{]}\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow \left(RhereditaryA\to \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)\right)$$
37	6 36	syl6ib	$$⊢\left(\forall f\left(Rhereditaryf\to \left(\forall a\left(XRa\to a\in f\right)\to Y\in f\right)\right)\leftrightarrow X\mathrm{t+}\left(R\right)Y\right)\to \left(X\mathrm{t+}\left(R\right)Y\to \left(RhereditaryA\to \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)\right)\right)$$
38	5 37	ax-mp	$$⊢X\mathrm{t+}\left(R\right)Y\to \left(RhereditaryA\to \left(\forall a\left(XRa\to a\in A\right)\to Y\in A\right)\right)$$