frege125

Description: Lemma for frege126 . Proposition 125 of Frege1879 p. 81. (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	frege125	$⊢ (X (t+ (R) \cup I) M \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \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	frege124	$⊢ Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to X (t+ (R) \cup I) M))$
6		frege20	$⊢ (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to X (t+ (R) \cup I) M))) \to ((X (t+ (R) \cup I) M \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)))))$
7	5 6	ax-mp	$⊢ (X (t+ (R) \cup I) M \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to (\neg X t+ (R) M \to M (t+ (R) \cup I) X))))$

Metamath Proof Explorer