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

Proof

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