Theorem frege91

Description: Every result of an application of a procedure R to an object X follows that X in the R -sequence. Proposition 91 of Frege1879 p. 68. (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	frege91	|- ( X R Y -> 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	2	frege63c	|- ( [. Y / a ]. X R a -> ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> [. Y / a ]. a e. f ) ) )
5		sbcbr2g	|- ( Y e. V -> ( [. Y / a ]. X R a <-> X R [_ Y / a ]_ a ) )
6		csbvarg	|- ( Y e. V -> [_ Y / a ]_ a = Y )
7	6	breq2d	|- ( Y e. V -> ( X R [_ Y / a ]_ a <-> X R Y ) )
8	5 7	bitrd	|- ( Y e. V -> ( [. Y / a ]. X R a <-> X R Y ) )
9	2 8	ax-mp	|- ( [. Y / a ]. X R a <-> X R Y )
10		sbcel1v	|- ( [. Y / a ]. a e. f <-> Y e. f )
11	10	imbi2i	|- ( ( A. a ( X R a -> a e. f ) -> [. Y / a ]. a e. f ) <-> ( A. a ( X R a -> a e. f ) -> Y e. f ) )
12	11	imbi2i	|- ( ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> [. Y / a ]. a e. f ) ) <-> ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) )
13	4 9 12	3imtr3i	|- ( X R Y -> ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) )
14	13	alrimiv	|- ( X R Y -> A. f ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) )
15	1 2 3	frege90	|- ( ( X R Y -> A. f ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) ) -> ( X R Y -> X ( t+ ` R ) Y ) )
16	14 15	ax-mp	|- ( X R Y -> X ( t+ ` R ) Y )