Theorem frege110

Description: Proposition 110 of Frege1879 p. 75. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege110.x	|- X e. A
	frege110.y	|- Y e. B
	frege110.m	|- M e. C
	frege110.r	|- R e. D
Assertion	frege110	|- ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) )

Proof

Step	Hyp	Ref	Expression
1		frege110.x	|- X e. A
2		frege110.y	|- Y e. B
3		frege110.m	|- M e. C
4		frege110.r	|- R e. D
5	1 4	frege109	|- R hereditary ( ( ( t+ ` R ) u. _I ) " { X } )
6		imaundir	|- ( ( ( t+ ` R ) u. _I ) " { X } ) = ( ( ( t+ ` R ) " { X } ) u. ( _I " { X } ) )
7		fvex	|- ( t+ ` R ) e. _V
8		imaexg	|- ( ( t+ ` R ) e. _V -> ( ( t+ ` R ) " { X } ) e. _V )
9	7 8	ax-mp	|- ( ( t+ ` R ) " { X } ) e. _V
10		imai	|- ( _I " { X } ) = { X }
11		snex	|- { X } e. _V
12	10 11	eqeltri	|- ( _I " { X } ) e. _V
13	9 12	unex	|- ( ( ( t+ ` R ) " { X } ) u. ( _I " { X } ) ) e. _V
14	6 13	eqeltri	|- ( ( ( t+ ` R ) u. _I ) " { X } ) e. _V
15	2 3 4 14	frege78	|- ( R hereditary ( ( ( t+ ` R ) u. _I ) " { X } ) -> ( A. a ( Y R a -> a e. ( ( ( t+ ` R ) u. _I ) " { X } ) ) -> ( Y ( t+ ` R ) M -> M e. ( ( ( t+ ` R ) u. _I ) " { X } ) ) ) )
16	1	elexi	|- X e. _V
17		vex	|- a e. _V
18	16 17	elimasn	|- ( a e. ( ( ( t+ ` R ) u. _I ) " { X } ) <-> <. X , a >. e. ( ( t+ ` R ) u. _I ) )
19		df-br	|- ( X ( ( t+ ` R ) u. _I ) a <-> <. X , a >. e. ( ( t+ ` R ) u. _I ) )
20	18 19	bitr4i	|- ( a e. ( ( ( t+ ` R ) u. _I ) " { X } ) <-> X ( ( t+ ` R ) u. _I ) a )
21	20	imbi2i	|- ( ( Y R a -> a e. ( ( ( t+ ` R ) u. _I ) " { X } ) ) <-> ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) )
22	21	albii	|- ( A. a ( Y R a -> a e. ( ( ( t+ ` R ) u. _I ) " { X } ) ) <-> A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) )
23	3	elexi	|- M e. _V
24	16 23	elimasn	|- ( M e. ( ( ( t+ ` R ) u. _I ) " { X } ) <-> <. X , M >. e. ( ( t+ ` R ) u. _I ) )
25		df-br	|- ( X ( ( t+ ` R ) u. _I ) M <-> <. X , M >. e. ( ( t+ ` R ) u. _I ) )
26	24 25	bitr4i	|- ( M e. ( ( ( t+ ` R ) u. _I ) " { X } ) <-> X ( ( t+ ` R ) u. _I ) M )
27	26	imbi2i	|- ( ( Y ( t+ ` R ) M -> M e. ( ( ( t+ ` R ) u. _I ) " { X } ) ) <-> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) )
28	15 22 27	3imtr3g	|- ( R hereditary ( ( ( t+ ` R ) u. _I ) " { X } ) -> ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) )
29	5 28	ax-mp	|- ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) )