Metamath Proof Explorer

Theorem frnssb

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 frnssb ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V → F : A ⟶ W ↔ F : A ⟶ V

Proof

Step Hyp Ref Expression
1 simpr ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V → ∀ k ∈ A F ⁡ k ∈ V
2 ffn ⊢ F : A ⟶ W → F Fn A
3 1 2 anim12ci ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V ∧ F : A ⟶ W → F Fn A ∧ ∀ k ∈ A F ⁡ k ∈ V
4 ffnfv ⊢ F : A ⟶ V ↔ F Fn A ∧ ∀ k ∈ A F ⁡ k ∈ V
5 3 4 sylibr ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V ∧ F : A ⟶ W → F : A ⟶ V
6 simpl ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V → V ⊆ W
7 6 anim1ci ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V ∧ F : A ⟶ V → F : A ⟶ V ∧ V ⊆ W
8 fss ⊢ F : A ⟶ V ∧ V ⊆ W → F : A ⟶ W
9 7 8 syl ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V ∧ F : A ⟶ V → F : A ⟶ W
10 5 9 impbida ⊢ V ⊆ W ∧ ∀ k ∈ A F ⁡ k ∈ V → F : A ⟶ W ↔ F : A ⟶ V