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	$⊢ M \in U$
	frege130.r	$⊢ R \in V$
Assertion	frege132	$⊢ (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))) \to (Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))))$

Step	Hyp	Ref	Expression
1		frege130.m	$⊢ M \in U$
2		frege130.r	$⊢ R \in V$
3	1 2	frege131	$⊢ Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])$
4		frege9	$⊢ (Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \to ((R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))) \to (Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))))$
5	3 4	ax-mp	$⊢ (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))) \to (Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))))$

Metamath Proof Explorer