Metamath Proof Explorer

Theorem frege86

Description: Conclusion about element one past Y in the R -sequence. Proposition 86 of Frege1879 p. 66. (Contributed by RP, 1-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	frege86.x	$⊢ X \in U$
		frege86.y	$⊢ Y \in V$
		frege86.r	$⊢ R \in W$
		frege86.a	$⊢ A \in B$
	Assertion	frege86	$⊢ ((R hereditary A \to Y \in A) \to (R hereditary A \to (Y R Z \to Z \in A))) \to (X t+ (R) Y \to (\forall w (X R w \to w \in A) \to (R hereditary A \to (Y R Z \to Z \in A))))$

Proof

Step	Hyp	Ref	Expression
1		frege86.x	$⊢ X \in U$
2		frege86.y	$⊢ Y \in V$
3		frege86.r	$⊢ R \in W$
4		frege86.a	$⊢ A \in B$
5	1 2 3 4	frege85	$⊢ X t+ (R) Y \to (\forall w (X R w \to w \in A) \to (R hereditary A \to Y \in A))$
6		frege19	$⊢ (X t+ (R) Y \to (\forall w (X R w \to w \in A) \to (R hereditary A \to Y \in A))) \to (((R hereditary A \to Y \in A) \to (R hereditary A \to (Y R Z \to Z \in A))) \to (X t+ (R) Y \to (\forall w (X R w \to w \in A) \to (R hereditary A \to (Y R Z \to Z \in A)))))$
7	5 6	ax-mp	$⊢ ((R hereditary A \to Y \in A) \to (R hereditary A \to (Y R Z \to Z \in A))) \to (X t+ (R) Y \to (\forall w (X R w \to w \in A) \to (R hereditary A \to (Y R Z \to Z \in A))))$