Metamath Proof Explorer


Theorem frege95

Description: Looking one past a pair related by transitive closure of a relation. Proposition 95 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege95.x X U
frege95.y Y V
frege95.z Z W
frege95.r R A
Assertion frege95 Y R Z X t+ R Y X t+ R Z

Proof

Step Hyp Ref Expression
1 frege95.x X U
2 frege95.y Y V
3 frege95.z Z W
4 frege95.r R A
5 vex f V
6 1 2 3 4 5 frege88 Y R Z X t+ R Y w X R w w f R hereditary f Z f
7 6 alrimdv Y R Z X t+ R Y f w X R w w f R hereditary f Z f
8 1 3 4 frege94 Y R Z X t+ R Y f w X R w w f R hereditary f Z f Y R Z X t+ R Y X t+ R Z
9 7 8 ax-mp Y R Z X t+ R Y X t+ R Z