Metamath Proof Explorer


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 dfss2
 |-  ( ( 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 )