frege123

Description: Lemma for frege124 . Proposition 123 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege123.x	$⊢ X \in U$
	frege123.y	$⊢ Y \in V$
Assertion	frege123	$⊢ (\forall a (Y R a \to X (t+ (R) \cup I) a) \to (Y t+ (R) M \to X (t+ (R) \cup I) M)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to X (t+ (R) \cup I) M)))$

Step	Hyp	Ref	Expression
1		frege123.x	$⊢ X \in U$
2		frege123.y	$⊢ Y \in V$
3		vex	$⊢ a \in V$
4	1 2 3	frege122	$⊢ Fun {R^{-1}}^{-1} \to (Y R X \to (Y R a \to X (t+ (R) \cup I) a))$
5	4	alrimdv	$⊢ Fun {R^{-1}}^{-1} \to (Y R X \to \forall a (Y R a \to X (t+ (R) \cup I) a))$
6		frege19	$⊢ (Fun {R^{-1}}^{-1} \to (Y R X \to \forall a (Y R a \to X (t+ (R) \cup I) a))) \to ((\forall a (Y R a \to X (t+ (R) \cup I) a) \to (Y t+ (R) M \to X (t+ (R) \cup I) M)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to X (t+ (R) \cup I) M))))$
7	5 6	ax-mp	$⊢ (\forall a (Y R a \to X (t+ (R) \cup I) a) \to (Y t+ (R) M \to X (t+ (R) \cup I) M)) \to (Fun {R^{-1}}^{-1} \to (Y R X \to (Y t+ (R) M \to X (t+ (R) \cup I) M)))$

Metamath Proof Explorer