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

Metamath Proof Explorer

Theorem fcdmssb

Description: A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021)

Ref Expression
Assertion fcdmssb 
|- ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> ( F : A --> W <-> F : A --> V ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> A. k e. A ( F ` k ) e. V )
2 ffn 
 |-  ( F : A --> W -> F Fn A )
3 1 2 anim12ci 
 |-  ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> W ) -> ( F Fn A /\ A. k e. A ( F ` k ) e. V ) )
4 ffnfv 
 |-  ( F : A --> V <-> ( F Fn A /\ A. k e. A ( F ` k ) e. V ) )
5 3 4 sylibr 
 |-  ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> W ) -> F : A --> V )
6 simpl 
 |-  ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> V C_ W )
7 6 anim1ci 
 |-  ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> V ) -> ( F : A --> V /\ V C_ W ) )
8 fss 
 |-  ( ( F : A --> V /\ V C_ W ) -> F : A --> W )
9 7 8 syl 
 |-  ( ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) /\ F : A --> V ) -> F : A --> W )
10 5 9 impbida 
 |-  ( ( V C_ W /\ A. k e. A ( F ` k ) e. V ) -> ( F : A --> W <-> F : A --> V ) )