Metamath Proof Explorer


Theorem frege132

Description: Lemma for frege133 . Proposition 132 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m M U
frege130.r R V
Assertion frege132 R hereditary t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y

Proof

Step Hyp Ref Expression
1 frege130.m M U
2 frege130.r R V
3 1 2 frege131 Fun R -1 -1 R hereditary t+ R -1 M t+ R I M
4 frege9 Fun R -1 -1 R hereditary t+ R -1 M t+ R I M R hereditary t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y
5 3 4 ax-mp R hereditary t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y