Metamath Proof Explorer


Theorem frege98

Description: If Y follows X and Z follows Y in the R -sequence then Z follows X in the R -sequence because the transitive closure of a relation has the transitive property. Proposition 98 of Frege1879 p. 71. (Contributed by RP, 2-Jul-2020) (Revised by RP, 6-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege98.x X A
frege98.y Y B
frege98.z Z C
frege98.r R D
Assertion frege98 X t+ R Y Y t+ R Z X t+ R Z

Proof

Step Hyp Ref Expression
1 frege98.x X A
2 frege98.y Y B
3 frege98.z Z C
4 frege98.r R D
5 1 4 frege97 R hereditary t+ R X
6 fvex t+ R V
7 imaexg t+ R V t+ R X V
8 6 7 ax-mp t+ R X V
9 2 3 4 8 frege84 R hereditary t+ R X Y t+ R X Y t+ R Z Z t+ R X
10 5 9 ax-mp Y t+ R X Y t+ R Z Z t+ R X
11 1 elexi X V
12 2 elexi Y V
13 11 12 elimasn Y t+ R X X Y t+ R
14 df-br X t+ R Y X Y t+ R
15 13 14 bitr4i Y t+ R X X t+ R Y
16 3 elexi Z V
17 11 16 elimasn Z t+ R X X Z t+ R
18 df-br X t+ R Z X Z t+ R
19 17 18 bitr4i Z t+ R X X t+ R Z
20 19 imbi2i Y t+ R Z Z t+ R X Y t+ R Z X t+ R Z
21 10 15 20 3imtr3i X t+ R Y Y t+ R Z X t+ R Z