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