Theorem frege94

Description: Looking one past a pair related by transitive closure of a relation. Proposition 94 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege94.x	|- X e. U
	frege94.z	|- Z e. V
	frege94.r	|- R e. W
Assertion	frege94	|- ( ( Y R Z -> ( X ( t+ ` R ) Y -> A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) ) ) -> ( Y R Z -> ( X ( t+ ` R ) Y -> X ( t+ ` R ) Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege94.x	|- X e. U
2		frege94.z	|- Z e. V
3		frege94.r	|- R e. W
4	1 2 3	frege93	|- ( A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) -> X ( t+ ` R ) Z )
5		frege7	|- ( ( A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) -> X ( t+ ` R ) Z ) -> ( ( Y R Z -> ( X ( t+ ` R ) Y -> A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) ) ) -> ( Y R Z -> ( X ( t+ ` R ) Y -> X ( t+ ` R ) Z ) ) ) )
6	4 5	ax-mp	|- ( ( Y R Z -> ( X ( t+ ` R ) Y -> A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) ) ) -> ( Y R Z -> ( X ( t+ ` R ) Y -> X ( t+ ` R ) Z ) ) )