Theorem frege97

Description: The property of following X in the R -sequence is hereditary in the R -sequence. Proposition 97 of Frege1879 p. 71.

Here we introduce the image of a singleton under a relation as class which stands for the property of following X in the R -sequence. (Contributed by RP, 2-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege97.x	|- X e. U
	frege97.r	|- R e. W
Assertion	frege97	|- R hereditary ( ( t+ ` R ) " { X } )

Proof

Step	Hyp	Ref	Expression
1		frege97.x	|- X e. U
2		frege97.r	|- R e. W
3		frege75	|- ( A. b ( b e. ( ( t+ ` R ) " { X } ) -> A. a ( b R a -> a e. ( ( t+ ` R ) " { X } ) ) ) -> R hereditary ( ( t+ ` R ) " { X } ) )
4		vex	|- b e. _V
5		vex	|- a e. _V
6	1 4 5 2	frege96	|- ( X ( t+ ` R ) b -> ( b R a -> X ( t+ ` R ) a ) )
7		df-br	|- ( X ( t+ ` R ) b <-> <. X , b >. e. ( t+ ` R ) )
8	1	elexi	|- X e. _V
9	8 4	elimasn	|- ( b e. ( ( t+ ` R ) " { X } ) <-> <. X , b >. e. ( t+ ` R ) )
10	7 9	bitr4i	|- ( X ( t+ ` R ) b <-> b e. ( ( t+ ` R ) " { X } ) )
11		df-br	|- ( X ( t+ ` R ) a <-> <. X , a >. e. ( t+ ` R ) )
12	8 5	elimasn	|- ( a e. ( ( t+ ` R ) " { X } ) <-> <. X , a >. e. ( t+ ` R ) )
13	11 12	bitr4i	|- ( X ( t+ ` R ) a <-> a e. ( ( t+ ` R ) " { X } ) )
14	13	imbi2i	|- ( ( b R a -> X ( t+ ` R ) a ) <-> ( b R a -> a e. ( ( t+ ` R ) " { X } ) ) )
15	6 10 14	3imtr3i	|- ( b e. ( ( t+ ` R ) " { X } ) -> ( b R a -> a e. ( ( t+ ` R ) " { X } ) ) )
16	15	alrimiv	|- ( b e. ( ( t+ ` R ) " { X } ) -> A. a ( b R a -> a e. ( ( t+ ` R ) " { X } ) ) )
17	3 16	mpg	|- R hereditary ( ( t+ ` R ) " { X } )