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 ⊢ φ → F : A ⟶ B
fssrescdmd.c ⊢ φ → C ⊆ A
fssrescdmd.d ⊢ φ → F C ⊆ D
Assertion fssrescdmd ⊢ φ → F ↾ C : C ⟶ D

Proof

Step Hyp Ref Expression
1 fssrescdmd.f ⊢ φ → F : A ⟶ B
2 fssrescdmd.c ⊢ φ → C ⊆ A
3 fssrescdmd.d ⊢ φ → F C ⊆ D
4 1 ffnd ⊢ φ → F Fn A
5 4 2 fnssresd ⊢ φ → F ↾ C Fn C
6 resima ⊢ F ↾ C C = F C
7 6 3 eqsstrid ⊢ φ → F ↾ C C ⊆ D
8 1 ffund ⊢ φ → Fun ⁡ F
9 8 funresd ⊢ φ → Fun ⁡ F ↾ C
10 1 fdmd ⊢ φ → dom ⁡ F = A
11 2 10 sseqtrrd ⊢ φ → C ⊆ dom ⁡ F
12 ssdmres ⊢ C ⊆ dom ⁡ F ↔ dom ⁡ F ↾ C = C
13 12 a1i ⊢ φ → C ⊆ dom ⁡ F ↔ dom ⁡ F ↾ C = C
14 eqcom ⊢ dom ⁡ F ↾ C = C ↔ C = dom ⁡ F ↾ C
15 13 14 bitrdi ⊢ φ → C ⊆ dom ⁡ F ↔ C = dom ⁡ F ↾ C
16 11 15 mpbid ⊢ φ → C = dom ⁡ F ↾ C
17 16 eqimssd ⊢ φ → C ⊆ dom ⁡ F ↾ C
18 funimass4 ⊢ Fun ⁡ F ↾ C ∧ C ⊆ dom ⁡ F ↾ C → F ↾ C C ⊆ D ↔ ∀ x ∈ C F ↾ C ⁡ x ∈ D
19 9 17 18 syl2anc ⊢ φ → F ↾ C C ⊆ D ↔ ∀ x ∈ C F ↾ C ⁡ x ∈ D
20 7 19 mpbid ⊢ φ → ∀ x ∈ C F ↾ C ⁡ x ∈ D
21 ffnfv ⊢ F ↾ C : C ⟶ D ↔ F ↾ C Fn C ∧ ∀ x ∈ C F ↾ C ⁡ x ∈ D
22 5 20 21 sylanbrc ⊢ φ → F ↾ C : C ⟶ D