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 MU
frege130.r RV
Assertion frege132 Rhereditaryt+R-1Mt+RIMXt+RMXt+RY¬Yt+RMMt+RIYFunR-1-1Xt+RMXt+RY¬Yt+RMMt+RIY

Proof

Step Hyp Ref Expression
1 frege130.m MU
2 frege130.r RV
3 1 2 frege131 FunR-1-1Rhereditaryt+R-1Mt+RIM
4 frege9 FunR-1-1Rhereditaryt+R-1Mt+RIMRhereditaryt+R-1Mt+RIMXt+RMXt+RY¬Yt+RMMt+RIYFunR-1-1Xt+RMXt+RY¬Yt+RMMt+RIY
5 3 4 ax-mp Rhereditaryt+R-1Mt+RIMXt+RMXt+RY¬Yt+RMMt+RIYFunR-1-1Xt+RMXt+RY¬Yt+RMMt+RIY