Theorem dffrege76

Description: If from the two propositions that every result of an application of the procedure R to B has property f and that property f is hereditary in the R -sequence, it can be inferred, whatever f may be, that E has property f , then we say E follows B in the R -sequence. Definition 76 of Frege1879 p. 60.

Each of B , E and R must be sets. (Contributed by RP, 2-Jul-2020)

	Ref	Expression
Hypotheses	frege76.b	$$⊢B\in U$$
	frege76.e	$$⊢E\in V$$
	frege76.r	$$⊢R\in W$$
Assertion	dffrege76	$$⊢\forall f\left(Rhereditaryf\to \left(\forall a\left(BRa\to a\in f\right)\to E\in f\right)\right)\leftrightarrow B\mathrm{t+}\left(R\right)E$$

Proof

Step	Hyp	Ref	Expression
1		frege76.b	$$⊢B\in U$$
2		frege76.e	$$⊢E\in V$$
3		frege76.r	$$⊢R\in W$$
4		brtrclfv2	$$⊢\left(B\in U\wedge E\in V\wedge R\in W\right)\to \left(B\mathrm{t+}\left(R\right)E\leftrightarrow E\in \bigcap \left\{f|R\left[\left\{B\right\}\cup f\right]\subseteq f\right\}\right)$$
5	1 2 3 4	mp3an	$$⊢B\mathrm{t+}\left(R\right)E\leftrightarrow E\in \bigcap \left\{f|R\left[\left\{B\right\}\cup f\right]\subseteq f\right\}$$
6	2	elexi	$$⊢E\in \mathrm{V}$$
7	6	elintab	$$⊢E\in \bigcap \left\{f|R\left[\left\{B\right\}\cup f\right]\subseteq f\right\}\leftrightarrow \forall f\left(R\left[\left\{B\right\}\cup f\right]\subseteq f\to E\in f\right)$$
8		imaundi	$$⊢R\left[\left\{B\right\}\cup f\right]=R\left[\left\{B\right\}\right]\cup R\left[f\right]$$
9	8	equncomi	$$⊢R\left[\left\{B\right\}\cup f\right]=R\left[f\right]\cup R\left[\left\{B\right\}\right]$$
10	9	sseq1i	$$⊢R\left[\left\{B\right\}\cup f\right]\subseteq f\leftrightarrow R\left[f\right]\cup R\left[\left\{B\right\}\right]\subseteq f$$
11		unss	$$⊢\left(R\left[f\right]\subseteq f\wedge R\left[\left\{B\right\}\right]\subseteq f\right)\leftrightarrow R\left[f\right]\cup R\left[\left\{B\right\}\right]\subseteq f$$
12	10 11	bitr4i	$$⊢R\left[\left\{B\right\}\cup f\right]\subseteq f\leftrightarrow \left(R\left[f\right]\subseteq f\wedge R\left[\left\{B\right\}\right]\subseteq f\right)$$
13		df-he	$$⊢Rhereditaryf\leftrightarrow R\left[f\right]\subseteq f$$
14	13	bicomi	$$⊢R\left[f\right]\subseteq f\leftrightarrow Rhereditaryf$$
15		df-ss	$$⊢R\left[\left\{B\right\}\right]\subseteq f\leftrightarrow \forall a\left(a\in R\left[\left\{B\right\}\right]\to a\in f\right)$$
16	1	elexi	$$⊢B\in \mathrm{V}$$
17		vex	$$⊢a\in \mathrm{V}$$
18	16 17	elimasn	$$⊢a\in R\left[\left\{B\right\}\right]\leftrightarrow ⟨B,a⟩\in R$$
19		df-br	$$⊢BRa\leftrightarrow ⟨B,a⟩\in R$$
20	18 19	bitr4i	$$⊢a\in R\left[\left\{B\right\}\right]\leftrightarrow BRa$$
21	20	imbi1i	$$⊢\left(a\in R\left[\left\{B\right\}\right]\to a\in f\right)\leftrightarrow \left(BRa\to a\in f\right)$$
22	21	albii	$$⊢\forall a\left(a\in R\left[\left\{B\right\}\right]\to a\in f\right)\leftrightarrow \forall a\left(BRa\to a\in f\right)$$
23	15 22	bitri	$$⊢R\left[\left\{B\right\}\right]\subseteq f\leftrightarrow \forall a\left(BRa\to a\in f\right)$$
24	14 23	anbi12i	$$⊢\left(R\left[f\right]\subseteq f\wedge R\left[\left\{B\right\}\right]\subseteq f\right)\leftrightarrow \left(Rhereditaryf\wedge \forall a\left(BRa\to a\in f\right)\right)$$
25	12 24	bitri	$$⊢R\left[\left\{B\right\}\cup f\right]\subseteq f\leftrightarrow \left(Rhereditaryf\wedge \forall a\left(BRa\to a\in f\right)\right)$$
26	25	imbi1i	$$⊢\left(R\left[\left\{B\right\}\cup f\right]\subseteq f\to E\in f\right)\leftrightarrow \left(\left(Rhereditaryf\wedge \forall a\left(BRa\to a\in f\right)\right)\to E\in f\right)$$
27		impexp	$$⊢\left(\left(Rhereditaryf\wedge \forall a\left(BRa\to a\in f\right)\right)\to E\in f\right)\leftrightarrow \left(Rhereditaryf\to \left(\forall a\left(BRa\to a\in f\right)\to E\in f\right)\right)$$
28	26 27	bitri	$$⊢\left(R\left[\left\{B\right\}\cup f\right]\subseteq f\to E\in f\right)\leftrightarrow \left(Rhereditaryf\to \left(\forall a\left(BRa\to a\in f\right)\to E\in f\right)\right)$$
29	28	albii	$$⊢\forall f\left(R\left[\left\{B\right\}\cup f\right]\subseteq f\to E\in f\right)\leftrightarrow \forall f\left(Rhereditaryf\to \left(\forall a\left(BRa\to a\in f\right)\to E\in f\right)\right)$$
30	5 7 29	3bitrri	$$⊢\forall f\left(Rhereditaryf\to \left(\forall a\left(BRa\to a\in f\right)\to E\in f\right)\right)\leftrightarrow B\mathrm{t+}\left(R\right)E$$