Metamath Proof Explorer

Theorem frege109

Description: The property of belonging to the R -sequence beginning with X is hereditary in the R -sequence. Proposition 109 of Frege1879 p. 74. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	frege109.x	$⊢ X \in U$
		frege109.r	$⊢ R \in V$
	Assertion	frege109	$⊢ R hereditary (t+ (R) \cup I) [\{X\}]$

Proof

Step	Hyp	Ref	Expression
1		frege109.x	$⊢ X \in U$
2		frege109.r	$⊢ R \in V$
3		frege75	$⊢ \forall y (y \in (t+ (R) \cup I) [\{X\}] \to \forall z (y R z \to z \in (t+ (R) \cup I) [\{X\}])) \to R hereditary (t+ (R) \cup I) [\{X\}]$
4		vex	$⊢ y \in V$
5		vex	$⊢ z \in V$
6	1 4 5 2	frege108	$⊢ X (t+ (R) \cup I) y \to (y R z \to X (t+ (R) \cup I) z)$
7		df-br	$⊢ X (t+ (R) \cup I) y \leftrightarrow ⟨X, y⟩ \in (t+ (R) \cup I)$
8	1	elexi	$⊢ X \in V$
9	8 4	elimasn	$⊢ y \in (t+ (R) \cup I) [\{X\}] \leftrightarrow ⟨X, y⟩ \in (t+ (R) \cup I)$
10	7 9	bitr4i	$⊢ X (t+ (R) \cup I) y \leftrightarrow y \in (t+ (R) \cup I) [\{X\}]$
11		df-br	$⊢ X (t+ (R) \cup I) z \leftrightarrow ⟨X, z⟩ \in (t+ (R) \cup I)$
12	8 5	elimasn	$⊢ z \in (t+ (R) \cup I) [\{X\}] \leftrightarrow ⟨X, z⟩ \in (t+ (R) \cup I)$
13	11 12	bitr4i	$⊢ X (t+ (R) \cup I) z \leftrightarrow z \in (t+ (R) \cup I) [\{X\}]$
14	13	imbi2i	$⊢ (y R z \to X (t+ (R) \cup I) z) \leftrightarrow (y R z \to z \in (t+ (R) \cup I) [\{X\}])$
15	6 10 14	3imtr3i	$⊢ y \in (t+ (R) \cup I) [\{X\}] \to (y R z \to z \in (t+ (R) \cup I) [\{X\}])$
16	15	alrimiv	$⊢ y \in (t+ (R) \cup I) [\{X\}] \to \forall z (y R z \to z \in (t+ (R) \cup I) [\{X\}])$
17	3 16	mpg	$⊢ R hereditary (t+ (R) \cup I) [\{X\}]$