Theorem ffvresb

Description: A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Assertion	ffvresb	⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fdm	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 → dom ( 𝐹 ↾ 𝐴 ) = 𝐴 )
2		dmres	⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
3		inss2	⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ dom 𝐹
4	2 3	eqsstri	⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹
5	1 4	eqsstrrdi	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 → 𝐴 ⊆ dom 𝐹 )
6	5	sselda	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 )
7		fvres	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8	7	adantl	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9		ffvelcdm	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 )
10	8 9	eqeltrrd	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11	6 10	jca	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
12	11	ralrimiva	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
13		simpl	⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → 𝑥 ∈ dom 𝐹 )
14	13	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝐹 )
15		dfss3	⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝐹 )
16	14 15	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → 𝐴 ⊆ dom 𝐹 )
17		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
18		fnssres	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
19	17 18	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
20	16 19	sylan2	⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
21		simpr	⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
22	7	eleq1d	⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
23	21 22	imbitrrid	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 ) )
24	23	ralimia	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 )
25	24	adantl	⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 )
26		fnfvrnss	⊢ ( ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ 𝐵 )
27	20 25 26	syl2anc	⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ 𝐵 )
28		df-f	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ran ( 𝐹 ↾ 𝐴 ) ⊆ 𝐵 ) )
29	20 27 28	sylanbrc	⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
30	29	ex	⊢ ( Fun 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ) )
31	12 30	impbid2	⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )