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

Metamath Proof Explorer

Theorem fnssintima

Description: Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024)

Ref Expression
Assertion fnssintima 
|- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 ssint 
 |-  ( C C_ |^| ( F " B ) <-> A. y e. ( F " B ) C C_ y )
2 df-ral 
 |-  ( A. y e. ( F " B ) C C_ y <-> A. y ( y e. ( F " B ) -> C C_ y ) )
3 1 2 bitri 
 |-  ( C C_ |^| ( F " B ) <-> A. y ( y e. ( F " B ) -> C C_ y ) )
4 fvelimab 
 |-  ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) )
5 4 imbi1d 
 |-  ( ( F Fn A /\ B C_ A ) -> ( ( y e. ( F " B ) -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) ) )
6 5 albidv 
 |-  ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) ) )
7 ralcom4 
 |-  ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) )
8 eqcom 
 |-  ( ( F ` x ) = y <-> y = ( F ` x ) )
9 8 imbi1i 
 |-  ( ( ( F ` x ) = y -> C C_ y ) <-> ( y = ( F ` x ) -> C C_ y ) )
10 9 albii 
 |-  ( A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y ( y = ( F ` x ) -> C C_ y ) )
11 fvex 
 |-  ( F ` x ) e. _V
12 sseq2 
 |-  ( y = ( F ` x ) -> ( C C_ y <-> C C_ ( F ` x ) ) )
13 11 12 ceqsalv 
 |-  ( A. y ( y = ( F ` x ) -> C C_ y ) <-> C C_ ( F ` x ) )
14 10 13 bitri 
 |-  ( A. y ( ( F ` x ) = y -> C C_ y ) <-> C C_ ( F ` x ) )
15 14 ralbii 
 |-  ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) )
16 r19.23v 
 |-  ( A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) )
17 16 albii 
 |-  ( A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) )
18 7 15 17 3bitr3ri 
 |-  ( A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) )
19 6 18 bitrdi 
 |-  ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) ) )
20 3 19 bitrid 
 |-  ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) )