Theorem 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	⊢ 𝑋 ∈ 𝐴
	frege98.y	⊢ 𝑌 ∈ 𝐵
	frege98.z	⊢ 𝑍 ∈ 𝐶
	frege98.r	⊢ 𝑅 ∈ 𝐷
Assertion	frege98	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		frege98.x	⊢ 𝑋 ∈ 𝐴
2		frege98.y	⊢ 𝑌 ∈ 𝐵
3		frege98.z	⊢ 𝑍 ∈ 𝐶
4		frege98.r	⊢ 𝑅 ∈ 𝐷
5	1 4	frege97	⊢ 𝑅 hereditary ( ( t+ ‘ 𝑅 ) “ { 𝑋 } )
6		fvex	⊢ ( t+ ‘ 𝑅 ) ∈ V
7		imaexg	⊢ ( ( t+ ‘ 𝑅 ) ∈ V → ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∈ V )
8	6 7	ax-mp	⊢ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∈ V
9	2 3 4 8	frege84	⊢ ( 𝑅 hereditary ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ( 𝑌 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) ) )
10	5 9	ax-mp	⊢ ( 𝑌 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) )
11	1	elexi	⊢ 𝑋 ∈ V
12	2	elexi	⊢ 𝑌 ∈ V
13	11 12	elimasn	⊢ ( 𝑌 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( t+ ‘ 𝑅 ) )
14		df-br	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( t+ ‘ 𝑅 ) )
15	13 14	bitr4i	⊢ ( 𝑌 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )
16	3	elexi	⊢ 𝑍 ∈ V
17	11 16	elimasn	⊢ ( 𝑍 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑍 ⟩ ∈ ( t+ ‘ 𝑅 ) )
18		df-br	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ↔ ⟨ 𝑋 , 𝑍 ⟩ ∈ ( t+ ‘ 𝑅 ) )
19	17 18	bitr4i	⊢ ( 𝑍 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 )
20	19	imbi2i	⊢ ( ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) ↔ ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) )
21	10 15 20	3imtr3i	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑍 → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) )