Metamath Proof Explorer


Theorem frege109

Description: The property of belonging to the R -sequence beginning with X is hereditary in the R -sequence. Proposition 109 of Frege1879 p. 74. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege109.x X U
frege109.r R V
Assertion frege109 R hereditary t+ R I X

Proof

Step Hyp Ref Expression
1 frege109.x X U
2 frege109.r R V
3 frege75 y y t+ R I X z y R z z t+ R I X R hereditary t+ R I X
4 vex y V
5 vex z V
6 1 4 5 2 frege108 X t+ R I y y R z X t+ R I z
7 df-br X t+ R I y X y t+ R I
8 1 elexi X V
9 8 4 elimasn y t+ R I X X y t+ R I
10 7 9 bitr4i X t+ R I y y t+ R I X
11 df-br X t+ R I z X z t+ R I
12 8 5 elimasn z t+ R I X X z t+ R I
13 11 12 bitr4i X t+ R I z z t+ R I X
14 13 imbi2i y R z X t+ R I z y R z z t+ R I X
15 6 10 14 3imtr3i y t+ R I X y R z z t+ R I X
16 15 alrimiv y t+ R I X z y R z z t+ R I X
17 3 16 mpg R hereditary t+ R I X