frege98

Description: If Y follows X and Z follows Y in the R -sequence then Z follows X in the R -sequence because the transitive closure of a relation has the transitive property. Proposition 98 of Frege1879 p. 71. (Contributed by RP, 2-Jul-2020) (Revised by RP, 6-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege98.x	$⊢ X \in A$
	frege98.y	$⊢ Y \in B$
	frege98.z	$⊢ Z \in C$
	frege98.r	$⊢ R \in D$
Assertion	frege98	$⊢ X t+ (R) Y \to (Y t+ (R) Z \to X t+ (R) Z)$

Proof

Step	Hyp	Ref	Expression
1		frege98.x	$⊢ X \in A$
2		frege98.y	$⊢ Y \in B$
3		frege98.z	$⊢ Z \in C$
4		frege98.r	$⊢ R \in D$
5	1 4	frege97	$⊢ R hereditary t+ (R) [\{X\}]$
6		fvex	$⊢ t+ (R) \in V$
7		imaexg	$⊢ t+ (R) \in V \to t+ (R) [\{X\}] \in V$
8	6 7	ax-mp	$⊢ t+ (R) [\{X\}] \in V$
9	2 3 4 8	frege84	$⊢ R hereditary t+ (R) [\{X\}] \to (Y \in t+ (R) [\{X\}] \to (Y t+ (R) Z \to Z \in t+ (R) [\{X\}]))$
10	5 9	ax-mp	$⊢ Y \in t+ (R) [\{X\}] \to (Y t+ (R) Z \to Z \in t+ (R) [\{X\}])$
11	1	elexi	$⊢ X \in V$
12	2	elexi	$⊢ Y \in V$
13	11 12	elimasn	$⊢ Y \in t+ (R) [\{X\}] \leftrightarrow ⟨X, Y⟩ \in t+ (R)$
14		df-br	$⊢ X t+ (R) Y \leftrightarrow ⟨X, Y⟩ \in t+ (R)$
15	13 14	bitr4i	$⊢ Y \in t+ (R) [\{X\}] \leftrightarrow X t+ (R) Y$
16	3	elexi	$⊢ Z \in V$
17	11 16	elimasn	$⊢ Z \in t+ (R) [\{X\}] \leftrightarrow ⟨X, Z⟩ \in t+ (R)$
18		df-br	$⊢ X t+ (R) Z \leftrightarrow ⟨X, Z⟩ \in t+ (R)$
19	17 18	bitr4i	$⊢ Z \in t+ (R) [\{X\}] \leftrightarrow X t+ (R) Z$
20	19	imbi2i	$⊢ (Y t+ (R) Z \to Z \in t+ (R) [\{X\}]) \leftrightarrow (Y t+ (R) Z \to X t+ (R) Z)$
21	10 15 20	3imtr3i	$⊢ X t+ (R) Y \to (Y t+ (R) Z \to X t+ (R) Z)$

Metamath Proof Explorer

Theorem frege98

Proof