Theorem frege93

Description: Necessary condition for two elements to be related by the transitive closure. Proposition 93 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		frege91.x	|- X e. U
2		frege91.y	|- Y e. V
3		frege91.r	|- R e. W
4		vex	|- f e. _V
5	4	frege60c	|- ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> ( [. f / f ]. R hereditary f -> ( [. f / f ]. A. z ( X R z -> z e. f ) -> [. f / f ]. Y e. f ) ) )
6		sbcid	|- ( [. f / f ]. R hereditary f <-> R hereditary f )
7		sbcid	|- ( [. f / f ]. A. z ( X R z -> z e. f ) <-> A. z ( X R z -> z e. f ) )
8		sbcid	|- ( [. f / f ]. Y e. f <-> Y e. f )
9	7 8	imbi12i	|- ( ( [. f / f ]. A. z ( X R z -> z e. f ) -> [. f / f ]. Y e. f ) <-> ( A. z ( X R z -> z e. f ) -> Y e. f ) )
10	5 6 9	3imtr3g	|- ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> ( R hereditary f -> ( A. z ( X R z -> z e. f ) -> Y e. f ) ) )
11	10	axc4i	|- ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> A. f ( R hereditary f -> ( A. z ( X R z -> z e. f ) -> Y e. f ) ) )
12	1 2 3	frege90	|- ( ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> A. f ( R hereditary f -> ( A. z ( X R z -> z e. f ) -> Y e. f ) ) ) -> ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> X ( t+ ` R ) Y ) )
13	11 12	ax-mp	|- ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> X ( t+ ` R ) Y )