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 e. U
	frege76.e	|- E e. V
	frege76.r	|- R e. W
Assertion	dffrege76	|- ( A. f ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) <-> B ( t+ ` R ) E )

Proof

Step	Hyp	Ref	Expression
1		frege76.b	|- B e. U
2		frege76.e	|- E e. V
3		frege76.r	|- R e. W
4		brtrclfv2	|- ( ( B e. U /\ E e. V /\ R e. W ) -> ( B ( t+ ` R ) E <-> E e. |^| { f | ( R " ( { B } u. f ) ) C_ f } ) )
5	1 2 3 4	mp3an	|- ( B ( t+ ` R ) E <-> E e. |^| { f | ( R " ( { B } u. f ) ) C_ f } )
6	2	elexi	|- E e. _V
7	6	elintab	|- ( E e. |^| { f | ( R " ( { B } u. f ) ) C_ f } <-> A. f ( ( R " ( { B } u. f ) ) C_ f -> E e. f ) )
8		imaundi	|- ( R " ( { B } u. f ) ) = ( ( R " { B } ) u. ( R " f ) )
9	8	equncomi	|- ( R " ( { B } u. f ) ) = ( ( R " f ) u. ( R " { B } ) )
10	9	sseq1i	|- ( ( R " ( { B } u. f ) ) C_ f <-> ( ( R " f ) u. ( R " { B } ) ) C_ f )
11		unss	|- ( ( ( R " f ) C_ f /\ ( R " { B } ) C_ f ) <-> ( ( R " f ) u. ( R " { B } ) ) C_ f )
12	10 11	bitr4i	|- ( ( R " ( { B } u. f ) ) C_ f <-> ( ( R " f ) C_ f /\ ( R " { B } ) C_ f ) )
13		df-he	|- ( R hereditary f <-> ( R " f ) C_ f )
14	13	bicomi	|- ( ( R " f ) C_ f <-> R hereditary f )
15		df-ss	|- ( ( R " { B } ) C_ f <-> A. a ( a e. ( R " { B } ) -> a e. f ) )
16	1	elexi	|- B e. _V
17		vex	|- a e. _V
18	16 17	elimasn	|- ( a e. ( R " { B } ) <-> <. B , a >. e. R )
19		df-br	|- ( B R a <-> <. B , a >. e. R )
20	18 19	bitr4i	|- ( a e. ( R " { B } ) <-> B R a )
21	20	imbi1i	|- ( ( a e. ( R " { B } ) -> a e. f ) <-> ( B R a -> a e. f ) )
22	21	albii	|- ( A. a ( a e. ( R " { B } ) -> a e. f ) <-> A. a ( B R a -> a e. f ) )
23	15 22	bitri	|- ( ( R " { B } ) C_ f <-> A. a ( B R a -> a e. f ) )
24	14 23	anbi12i	|- ( ( ( R " f ) C_ f /\ ( R " { B } ) C_ f ) <-> ( R hereditary f /\ A. a ( B R a -> a e. f ) ) )
25	12 24	bitri	|- ( ( R " ( { B } u. f ) ) C_ f <-> ( R hereditary f /\ A. a ( B R a -> a e. f ) ) )
26	25	imbi1i	|- ( ( ( R " ( { B } u. f ) ) C_ f -> E e. f ) <-> ( ( R hereditary f /\ A. a ( B R a -> a e. f ) ) -> E e. f ) )
27		impexp	|- ( ( ( R hereditary f /\ A. a ( B R a -> a e. f ) ) -> E e. f ) <-> ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) )
28	26 27	bitri	|- ( ( ( R " ( { B } u. f ) ) C_ f -> E e. f ) <-> ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) )
29	28	albii	|- ( A. f ( ( R " ( { B } u. f ) ) C_ f -> E e. f ) <-> A. f ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) )
30	5 7 29	3bitrri	|- ( A. f ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) <-> B ( t+ ` R ) E )