This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )