Metamath Proof Explorer

Theorem fveqressseq

Description: If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020)

Ref Expression
Hypothesis fveqdmss.1 ⊢ 𝐷 = dom 𝐵
Assertion fveqressseq ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ↾ 𝐷 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 fveqdmss.1 ⊢ 𝐷 = dom 𝐵
2 1 fveqdmss ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → 𝐷 ⊆ dom 𝐴 )
3 dmres ⊢ dom ( 𝐴 ↾ 𝐷 ) = ( 𝐷 ∩ dom 𝐴 )
4 incom ⊢ ( 𝐷 ∩ dom 𝐴 ) = ( dom 𝐴 ∩ 𝐷 )
5 sseqin2 ⊢ ( 𝐷 ⊆ dom 𝐴 ↔ ( dom 𝐴 ∩ 𝐷 ) = 𝐷 )
6 5 biimpi ⊢ ( 𝐷 ⊆ dom 𝐴 → ( dom 𝐴 ∩ 𝐷 ) = 𝐷 )
7 4 6 eqtrid ⊢ ( 𝐷 ⊆ dom 𝐴 → ( 𝐷 ∩ dom 𝐴 ) = 𝐷 )
8 3 7 eqtrid ⊢ ( 𝐷 ⊆ dom 𝐴 → dom ( 𝐴 ↾ 𝐷 ) = 𝐷 )
9 8 1 eqtrdi ⊢ ( 𝐷 ⊆ dom 𝐴 → dom ( 𝐴 ↾ 𝐷 ) = dom 𝐵 )
10 2 9 syl ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → dom ( 𝐴 ↾ 𝐷 ) = dom 𝐵 )
11 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
12 11 adantl ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
13 id ⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
14 12 13 sylan9eq ⊢ ( ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
15 14 ex ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
16 15 ralimdva ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) → ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐷 ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
17 16 3impia ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐷 ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
18 2 7 syl ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝐷 ∩ dom 𝐴 ) = 𝐷 )
19 3 18 eqtrid ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → dom ( 𝐴 ↾ 𝐷 ) = 𝐷 )
20 19 raleqdv ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐷 ) ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
21 17 20 mpbird ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐷 ) ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
22 simpll ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → Fun 𝐵 )
23 1 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ dom 𝐵 )
24 23 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ dom 𝐵 )
25 24 adantl ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ dom 𝐵 )
26 simplr ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → ∅ ∉ ran 𝐵 )
27 nelrnfvne ⊢ ( ( Fun 𝐵 ∧ 𝑥 ∈ dom 𝐵 ∧ ∅ ∉ ran 𝐵 ) → ( 𝐵 ‘ 𝑥 ) ≠ ∅ )
28 22 25 26 27 syl3anc ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐵 ‘ 𝑥 ) ≠ ∅ )
29 neeq1 ⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( ( 𝐴 ‘ 𝑥 ) ≠ ∅ ↔ ( 𝐵 ‘ 𝑥 ) ≠ ∅ ) )
30 28 29 syl5ibrcom ⊢ ( ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ 𝑥 ) ≠ ∅ ) )
31 30 ralimdva ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ) → ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ ∅ ) )
32 31 3impia ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ ∅ )
33 fvn0ssdmfun ⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ ∅ → ( 𝐷 ⊆ dom 𝐴 ∧ Fun ( 𝐴 ↾ 𝐷 ) ) )
34 33 simprd ⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ ∅ → Fun ( 𝐴 ↾ 𝐷 ) )
35 32 34 syl ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → Fun ( 𝐴 ↾ 𝐷 ) )
36 simp1 ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → Fun 𝐵 )
37 eqfunfv ⊢ ( ( Fun ( 𝐴 ↾ 𝐷 ) ∧ Fun 𝐵 ) → ( ( 𝐴 ↾ 𝐷 ) = 𝐵 ↔ ( dom ( 𝐴 ↾ 𝐷 ) = dom 𝐵 ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐷 ) ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) ) )
38 35 36 37 syl2anc ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( ( 𝐴 ↾ 𝐷 ) = 𝐵 ↔ ( dom ( 𝐴 ↾ 𝐷 ) = dom 𝐵 ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐷 ) ( ( 𝐴 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) ) )
39 10 21 38 mpbir2and ⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ↾ 𝐷 ) = 𝐵 )