frege97

Description: The property of following X in the R -sequence is hereditary in the R -sequence. Proposition 97 of Frege1879 p. 71.

Here we introduce the image of a singleton under a relation as class which stands for the property of following X in the R -sequence. (Contributed by RP, 2-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege97.x	$⊢ X \in U$
	frege97.r	$⊢ R \in W$
Assertion	frege97	$⊢ R hereditary t+ (R) [\{X\}]$

Proof

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

Metamath Proof Explorer

Theorem frege97

Proof