Metamath Proof Explorer

Theorem fnfvintima

Description: Condition for a function value to equal the intersection of an image that contains it. (Contributed by BTernaryTau, 23-Jun-2026)

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

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( ( F ` C ) = |^| ( F " B ) -> ( F ` C ) C_ |^| ( F " B ) )
2 fnssintima 
 |-  ( ( F Fn A /\ B C_ A ) -> ( ( F ` C ) C_ |^| ( F " B ) <-> A. x e. B ( F ` C ) C_ ( F ` x ) ) )
3 2 3adant3 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( ( F ` C ) C_ |^| ( F " B ) <-> A. x e. B ( F ` C ) C_ ( F ` x ) ) )
4 1 3 imbitrid 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( ( F ` C ) = |^| ( F " B ) -> A. x e. B ( F ` C ) C_ ( F ` x ) ) )
5 3 biimprd 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( A. x e. B ( F ` C ) C_ ( F ` x ) -> ( F ` C ) C_ |^| ( F " B ) ) )
6 fnfvima 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( F ` C ) e. ( F " B ) )
7 intss1 
 |-  ( ( F ` C ) e. ( F " B ) -> |^| ( F " B ) C_ ( F ` C ) )
8 6 7 syl 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> |^| ( F " B ) C_ ( F ` C ) )
9 5 8 jctird 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( A. x e. B ( F ` C ) C_ ( F ` x ) -> ( ( F ` C ) C_ |^| ( F " B ) /\ |^| ( F " B ) C_ ( F ` C ) ) ) )
10 eqss 
 |-  ( ( F ` C ) = |^| ( F " B ) <-> ( ( F ` C ) C_ |^| ( F " B ) /\ |^| ( F " B ) C_ ( F ` C ) ) )
11 9 10 imbitrrdi 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( A. x e. B ( F ` C ) C_ ( F ` x ) -> ( F ` C ) = |^| ( F " B ) ) )
12 4 11 impbid 
 |-  ( ( F Fn A /\ B C_ A /\ C e. B ) -> ( ( F ` C ) = |^| ( F " B ) <-> A. x e. B ( F ` C ) C_ ( F ` x ) ) )