frege117

Description: Lemma for frege118 . Proposition 117 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	frege116.x	$⊢ X \in U$
	Assertion	frege117	$⊢ (\forall b (b R X \to \forall a (b R a \to a = X)) \to (Y R X \to \forall a (Y R a \to a = X))) \to (Fun {R^{-1}}^{-1} \to (Y R X \to \forall a (Y R a \to a = X)))$

Step	Hyp	Ref	Expression
1		frege116.x	$⊢ X \in U$
2	1	frege116	$⊢ Fun {R^{-1}}^{-1} \to \forall b (b R X \to \forall a (b R a \to a = X))$
3		frege9	$⊢ (Fun {R^{-1}}^{-1} \to \forall b (b R X \to \forall a (b R a \to a = X))) \to ((\forall b (b R X \to \forall a (b R a \to a = X)) \to (Y R X \to \forall a (Y R a \to a = X))) \to (Fun {R^{-1}}^{-1} \to (Y R X \to \forall a (Y R a \to a = X))))$
4	2 3	ax-mp	$⊢ (\forall b (b R X \to \forall a (b R a \to a = X)) \to (Y R X \to \forall a (Y R a \to a = X))) \to (Fun {R^{-1}}^{-1} \to (Y R X \to \forall a (Y R a \to a = X)))$

Metamath Proof Explorer