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

Metamath Proof Explorer

Theorem fssrescdmd

Description: Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025)

Ref Expression
Hypotheses fssrescdmd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fssrescdmd.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
fssrescdmd.d ⊢ ( 𝜑 → ( 𝐹 “ 𝐶 ) ⊆ 𝐷 )
Assertion fssrescdmd ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 )

Proof

Step Hyp Ref Expression
1 fssrescdmd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fssrescdmd.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 fssrescdmd.d ⊢ ( 𝜑 → ( 𝐹 “ 𝐶 ) ⊆ 𝐷 )
4 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
5 4 2 fnssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
6 resima ⊢ ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) = ( 𝐹 “ 𝐶 )
7 6 3 eqsstrid ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 )
8 1 ffund ⊢ ( 𝜑 → Fun 𝐹 )
9 8 funresd ⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝐶 ) )
10 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
11 2 10 sseqtrrd ⊢ ( 𝜑 → 𝐶 ⊆ dom 𝐹 )
12 ssdmres ⊢ ( 𝐶 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 )
13 12 a1i ⊢ ( 𝜑 → ( 𝐶 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ) )
14 eqcom ⊢ ( dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ↔ 𝐶 = dom ( 𝐹 ↾ 𝐶 ) )
15 13 14 bitrdi ⊢ ( 𝜑 → ( 𝐶 ⊆ dom 𝐹 ↔ 𝐶 = dom ( 𝐹 ↾ 𝐶 ) ) )
16 11 15 mpbid ⊢ ( 𝜑 → 𝐶 = dom ( 𝐹 ↾ 𝐶 ) )
17 16 eqimssd ⊢ ( 𝜑 → 𝐶 ⊆ dom ( 𝐹 ↾ 𝐶 ) )
18 funimass4 ⊢ ( ( Fun ( 𝐹 ↾ 𝐶 ) ∧ 𝐶 ⊆ dom ( 𝐹 ↾ 𝐶 ) ) → ( ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
19 9 17 18 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
20 7 19 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 )
21 ffnfv ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 ↔ ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
22 5 20 21 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 )