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	|- X e. A
	frege98.y	|- Y e. B
	frege98.z	|- Z e. C
	frege98.r	|- R e. D
Assertion	frege98	|- ( X ( t+ ` R ) Y -> ( Y ( t+ ` R ) Z -> X ( t+ ` R ) Z ) )

Proof

Step	Hyp	Ref	Expression
1		frege98.x	|- X e. A
2		frege98.y	|- Y e. B
3		frege98.z	|- Z e. C
4		frege98.r	|- R e. D
5	1 4	frege97	|- R hereditary ( ( t+ ` R ) " { X } )
6		fvex	|- ( t+ ` R ) e. _V
7		imaexg	|- ( ( t+ ` R ) e. _V -> ( ( t+ ` R ) " { X } ) e. _V )
8	6 7	ax-mp	|- ( ( t+ ` R ) " { X } ) e. _V
9	2 3 4 8	frege84	|- ( R hereditary ( ( t+ ` R ) " { X } ) -> ( Y e. ( ( t+ ` R ) " { X } ) -> ( Y ( t+ ` R ) Z -> Z e. ( ( t+ ` R ) " { X } ) ) ) )
10	5 9	ax-mp	|- ( Y e. ( ( t+ ` R ) " { X } ) -> ( Y ( t+ ` R ) Z -> Z e. ( ( t+ ` R ) " { X } ) ) )
11	1	elexi	|- X e. _V
12	2	elexi	|- Y e. _V
13	11 12	elimasn	|- ( Y e. ( ( t+ ` R ) " { X } ) <-> <. X , Y >. e. ( t+ ` R ) )
14		df-br	|- ( X ( t+ ` R ) Y <-> <. X , Y >. e. ( t+ ` R ) )
15	13 14	bitr4i	|- ( Y e. ( ( t+ ` R ) " { X } ) <-> X ( t+ ` R ) Y )
16	3	elexi	|- Z e. _V
17	11 16	elimasn	|- ( Z e. ( ( t+ ` R ) " { X } ) <-> <. X , Z >. e. ( t+ ` R ) )
18		df-br	|- ( X ( t+ ` R ) Z <-> <. X , Z >. e. ( t+ ` R ) )
19	17 18	bitr4i	|- ( Z e. ( ( t+ ` R ) " { X } ) <-> X ( t+ ` R ) Z )
20	19	imbi2i	|- ( ( Y ( t+ ` R ) Z -> Z e. ( ( t+ ` R ) " { X } ) ) <-> ( Y ( t+ ` R ) Z -> X ( t+ ` R ) Z ) )
21	10 15 20	3imtr3i	|- ( X ( t+ ` R ) Y -> ( Y ( t+ ` R ) Z -> X ( t+ ` R ) Z ) )