Metamath Proof Explorer

Theorem intimafv

Description: The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024)

Ref Expression
Assertion intimafv 
|- ( ( Fun F /\ A C_ dom F ) -> |^| ( F " A ) = |^|_ x e. A ( F ` x ) )

Proof

Step Hyp Ref Expression
1 dfimafn 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A ( F ` x ) = y } )
2 1 inteqd 
 |-  ( ( Fun F /\ A C_ dom F ) -> |^| ( F " A ) = |^| { y | E. x e. A ( F ` x ) = y } )
3 fvex 
 |-  ( F ` x ) e. _V
4 3 rgenw 
 |-  A. x e. A ( F ` x ) e. _V
5 iinabrex 
 |-  ( A. x e. A ( F ` x ) e. _V -> |^|_ x e. A ( F ` x ) = |^| { y | E. x e. A y = ( F ` x ) } )
6 4 5 ax-mp 
 |-  |^|_ x e. A ( F ` x ) = |^| { y | E. x e. A y = ( F ` x ) }
7 eqcom 
 |-  ( ( F ` x ) = y <-> y = ( F ` x ) )
8 7 rexbii 
 |-  ( E. x e. A ( F ` x ) = y <-> E. x e. A y = ( F ` x ) )
9 8 abbii 
 |-  { y | E. x e. A ( F ` x ) = y } = { y | E. x e. A y = ( F ` x ) }
10 9 inteqi 
 |-  |^| { y | E. x e. A ( F ` x ) = y } = |^| { y | E. x e. A y = ( F ` x ) }
11 6 10 eqtr4i 
 |-  |^|_ x e. A ( F ` x ) = |^| { y | E. x e. A ( F ` x ) = y }
12 2 11 eqtr4di 
 |-  ( ( Fun F /\ A C_ dom F ) -> |^| ( F " A ) = |^|_ x e. A ( F ` x ) )