frege128

Description: Lemma for frege129 . Proposition 128 of Frege1879 p. 83. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege123.x	$⊢ X \in U$
	frege123.y	$⊢ Y \in V$
	frege124.m	$⊢ M \in W$
	frege124.r	$⊢ R \in S$
Assertion	frege128	$⊢ (M (t+ (R) \cup I) Y \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))) \to (Fun {R^{-1}}^{-1} \to ((\neg Y t+ (R) M \to M (t+ (R) \cup I) Y) \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))))$

Step	Hyp	Ref	Expression
1		frege123.x	$⊢ X \in U$
2		frege123.y	$⊢ Y \in V$
3		frege124.m	$⊢ M \in W$
4		frege124.r	$⊢ R \in S$
5	1 2 3 4	frege127	$⊢ Fun {R^{-1}}^{-1} \to (Y t+ (R) M \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)))$
6		frege51	$⊢ (Fun {R^{-1}}^{-1} \to (Y t+ (R) M \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)))) \to ((M (t+ (R) \cup I) Y \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))) \to (Fun {R^{-1}}^{-1} \to ((\neg Y t+ (R) M \to M (t+ (R) \cup I) Y) \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)))))$
7	5 6	ax-mp	$⊢ (M (t+ (R) \cup I) Y \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))) \to (Fun {R^{-1}}^{-1} \to ((\neg Y t+ (R) M \to M (t+ (R) \cup I) Y) \to (Y R X \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))))$

Metamath Proof Explorer