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 ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑊 ↔ 𝐹 : 𝐴 ⟶ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝑊 → 𝐹 Fn 𝐴 )
3 1 2 anim12ci ⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑊 ) → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) )
4 ffnfv ⊢ ( 𝐹 : 𝐴 ⟶ 𝑉 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) )
5 3 4 sylibr ⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑊 ) → 𝐹 : 𝐴 ⟶ 𝑉 )
6 simpl ⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → 𝑉 ⊆ 𝑊 )
7 6 anim1ci ⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑉 ∧ 𝑉 ⊆ 𝑊 ) )
8 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑉 ∧ 𝑉 ⊆ 𝑊 ) → 𝐹 : 𝐴 ⟶ 𝑊 )
9 7 8 syl ⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑉 ) → 𝐹 : 𝐴 ⟶ 𝑊 )
10 5 9 impbida ⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑊 ↔ 𝐹 : 𝐴 ⟶ 𝑉 ) )