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

Metamath Proof Explorer

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 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )