Theorem imaiinfv

Description: Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	imaiinfv	|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( F ` x ) = |^| ( F " B ) )

Proof

Step	Hyp	Ref	Expression
1		fnssres	|- ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B )
2		fniinfv	|- ( ( F |` B ) Fn B -> |^|_ x e. B ( ( F |` B ) ` x ) = |^| ran ( F |` B ) )
3	1 2	syl	|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( ( F |` B ) ` x ) = |^| ran ( F |` B ) )
4		fvres	|- ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
5	4	iineq2i	|- |^|_ x e. B ( ( F |` B ) ` x ) = |^|_ x e. B ( F ` x )
6	5	eqcomi	|- |^|_ x e. B ( F ` x ) = |^|_ x e. B ( ( F |` B ) ` x )
7		df-ima	|- ( F " B ) = ran ( F |` B )
8	7	inteqi	|- |^| ( F " B ) = |^| ran ( F |` B )
9	3 6 8	3eqtr4g	|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( F ` x ) = |^| ( F " B ) )