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	⊢ 𝐵 ∈ 𝑈
	frege76.e	⊢ 𝐸 ∈ 𝑉
	frege76.r	⊢ 𝑅 ∈ 𝑊
Assertion	dffrege76	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝐸 ∈ 𝑓 ) ) ↔ 𝐵 ( t+ ‘ 𝑅 ) 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		frege76.b	⊢ 𝐵 ∈ 𝑈
2		frege76.e	⊢ 𝐸 ∈ 𝑉
3		frege76.r	⊢ 𝑅 ∈ 𝑊
4		brtrclfv2	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝐵 ( t+ ‘ 𝑅 ) 𝐸 ↔ 𝐸 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 } ) )
5	1 2 3 4	mp3an	⊢ ( 𝐵 ( t+ ‘ 𝑅 ) 𝐸 ↔ 𝐸 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
6	2	elexi	⊢ 𝐸 ∈ V
7	6	elintab	⊢ ( 𝐸 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 } ↔ ∀ 𝑓 ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 → 𝐸 ∈ 𝑓 ) )
8		imaundi	⊢ ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) = ( ( 𝑅 “ { 𝐵 } ) ∪ ( 𝑅 “ 𝑓 ) )
9	8	equncomi	⊢ ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) = ( ( 𝑅 “ 𝑓 ) ∪ ( 𝑅 “ { 𝐵 } ) )
10	9	sseq1i	⊢ ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( ( 𝑅 “ 𝑓 ) ∪ ( 𝑅 “ { 𝐵 } ) ) ⊆ 𝑓 )
11		unss	⊢ ( ( ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ∧ ( 𝑅 “ { 𝐵 } ) ⊆ 𝑓 ) ↔ ( ( 𝑅 “ 𝑓 ) ∪ ( 𝑅 “ { 𝐵 } ) ) ⊆ 𝑓 )
12	10 11	bitr4i	⊢ ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ∧ ( 𝑅 “ { 𝐵 } ) ⊆ 𝑓 ) )
13		df-he	⊢ ( 𝑅 hereditary 𝑓 ↔ ( 𝑅 “ 𝑓 ) ⊆ 𝑓 )
14	13	bicomi	⊢ ( ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ↔ 𝑅 hereditary 𝑓 )
15		dfss2	⊢ ( ( 𝑅 “ { 𝐵 } ) ⊆ 𝑓 ↔ ∀ 𝑎 ( 𝑎 ∈ ( 𝑅 “ { 𝐵 } ) → 𝑎 ∈ 𝑓 ) )
16	1	elexi	⊢ 𝐵 ∈ V
17		vex	⊢ 𝑎 ∈ V
18	16 17	elimasn	⊢ ( 𝑎 ∈ ( 𝑅 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝑎 ⟩ ∈ 𝑅 )
19		df-br	⊢ ( 𝐵 𝑅 𝑎 ↔ ⟨ 𝐵 , 𝑎 ⟩ ∈ 𝑅 )
20	18 19	bitr4i	⊢ ( 𝑎 ∈ ( 𝑅 “ { 𝐵 } ) ↔ 𝐵 𝑅 𝑎 )
21	20	imbi1i	⊢ ( ( 𝑎 ∈ ( 𝑅 “ { 𝐵 } ) → 𝑎 ∈ 𝑓 ) ↔ ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) )
22	21	albii	⊢ ( ∀ 𝑎 ( 𝑎 ∈ ( 𝑅 “ { 𝐵 } ) → 𝑎 ∈ 𝑓 ) ↔ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) )
23	15 22	bitri	⊢ ( ( 𝑅 “ { 𝐵 } ) ⊆ 𝑓 ↔ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) )
24	14 23	anbi12i	⊢ ( ( ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ∧ ( 𝑅 “ { 𝐵 } ) ⊆ 𝑓 ) ↔ ( 𝑅 hereditary 𝑓 ∧ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ) )
25	12 24	bitri	⊢ ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( 𝑅 hereditary 𝑓 ∧ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ) )
26	25	imbi1i	⊢ ( ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 → 𝐸 ∈ 𝑓 ) ↔ ( ( 𝑅 hereditary 𝑓 ∧ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ) → 𝐸 ∈ 𝑓 ) )
27		impexp	⊢ ( ( ( 𝑅 hereditary 𝑓 ∧ ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) ) → 𝐸 ∈ 𝑓 ) ↔ ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝐸 ∈ 𝑓 ) ) )
28	26 27	bitri	⊢ ( ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 → 𝐸 ∈ 𝑓 ) ↔ ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝐸 ∈ 𝑓 ) ) )
29	28	albii	⊢ ( ∀ 𝑓 ( ( 𝑅 “ ( { 𝐵 } ∪ 𝑓 ) ) ⊆ 𝑓 → 𝐸 ∈ 𝑓 ) ↔ ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝐸 ∈ 𝑓 ) ) )
30	5 7 29	3bitrri	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝐵 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝐸 ∈ 𝑓 ) ) ↔ 𝐵 ( t+ ‘ 𝑅 ) 𝐸 )