Theorem intimag

Description: Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimag	|- ( A. y ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( |^| A " B ) = |^| { x | E. a e. A x = ( a " B ) } )

Proof

Step	Hyp	Ref	Expression
1		r19.12	|- ( E. b e. B A. a e. A <. b , y >. e. a -> A. a e. A E. b e. B <. b , y >. e. a )
2		id	|- ( ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) )
3	1 2	impbid2	|- ( ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( E. b e. B A. a e. A <. b , y >. e. a <-> A. a e. A E. b e. B <. b , y >. e. a ) )
4		elimaint	|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )
5		elintima	|- ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )
6	3 4 5	3bitr4g	|- ( ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( y e. ( |^| A " B ) <-> y e. |^| { x | E. a e. A x = ( a " B ) } ) )
7	6	alimi	|- ( A. y ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> A. y ( y e. ( |^| A " B ) <-> y e. |^| { x | E. a e. A x = ( a " B ) } ) )
8		dfcleq	|- ( ( |^| A " B ) = |^| { x | E. a e. A x = ( a " B ) } <-> A. y ( y e. ( |^| A " B ) <-> y e. |^| { x | E. a e. A x = ( a " B ) } ) )
9	7 8	sylibr	|- ( A. y ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( |^| A " B ) = |^| { x | E. a e. A x = ( a " B ) } )