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 syl5bb
 |-  ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) )