Theorem fveqdmss

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 domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fveqdmss.1	⊢ 𝐷 = dom 𝐵
2		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑎 ) )
3		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑎 ) )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝑎 → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) ) )
5	4	rspcva	⊢ ( ( 𝑎 ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) )
6		nelrnfvne	⊢ ( ( Fun 𝐵 ∧ 𝑎 ∈ dom 𝐵 ∧ ∅ ∉ ran 𝐵 ) → ( 𝐵 ‘ 𝑎 ) ≠ ∅ )
7		n0	⊢ ( ( 𝐵 ‘ 𝑎 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) )
8		eleq2	⊢ ( ( 𝐵 ‘ 𝑎 ) = ( 𝐴 ‘ 𝑎 ) → ( 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) ↔ 𝑏 ∈ ( 𝐴 ‘ 𝑎 ) ) )
9	8	eqcoms	⊢ ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → ( 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) ↔ 𝑏 ∈ ( 𝐴 ‘ 𝑎 ) ) )
10		elfvdm	⊢ ( 𝑏 ∈ ( 𝐴 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 )
11	9 10	syl6bi	⊢ ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → ( 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) )
12	11	com12	⊢ ( 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) )
13	12	exlimiv	⊢ ( ∃ 𝑏 𝑏 ∈ ( 𝐵 ‘ 𝑎 ) → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) )
14	7 13	sylbi	⊢ ( ( 𝐵 ‘ 𝑎 ) ≠ ∅ → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) )
15	6 14	syl	⊢ ( ( Fun 𝐵 ∧ 𝑎 ∈ dom 𝐵 ∧ ∅ ∉ ran 𝐵 ) → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) )
16	15	3exp	⊢ ( Fun 𝐵 → ( 𝑎 ∈ dom 𝐵 → ( ∅ ∉ ran 𝐵 → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) ) ) )
17	16	com12	⊢ ( 𝑎 ∈ dom 𝐵 → ( Fun 𝐵 → ( ∅ ∉ ran 𝐵 → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) ) ) )
18	17 1	eleq2s	⊢ ( 𝑎 ∈ 𝐷 → ( Fun 𝐵 → ( ∅ ∉ ran 𝐵 → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → 𝑎 ∈ dom 𝐴 ) ) ) )
19	18	com24	⊢ ( 𝑎 ∈ 𝐷 → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → ( ∅ ∉ ran 𝐵 → ( Fun 𝐵 → 𝑎 ∈ dom 𝐴 ) ) ) )
20	19	adantr	⊢ ( ( 𝑎 ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑎 ) → ( ∅ ∉ ran 𝐵 → ( Fun 𝐵 → 𝑎 ∈ dom 𝐴 ) ) ) )
21	5 20	mpd	⊢ ( ( 𝑎 ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( ∅ ∉ ran 𝐵 → ( Fun 𝐵 → 𝑎 ∈ dom 𝐴 ) ) )
22	21	ex	⊢ ( 𝑎 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( ∅ ∉ ran 𝐵 → ( Fun 𝐵 → 𝑎 ∈ dom 𝐴 ) ) ) )
23	22	com23	⊢ ( 𝑎 ∈ 𝐷 → ( ∅ ∉ ran 𝐵 → ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( Fun 𝐵 → 𝑎 ∈ dom 𝐴 ) ) ) )
24	23	com14	⊢ ( Fun 𝐵 → ( ∅ ∉ ran 𝐵 → ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ( 𝑎 ∈ 𝐷 → 𝑎 ∈ dom 𝐴 ) ) ) )
25	24	3imp	⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝑎 ∈ 𝐷 → 𝑎 ∈ dom 𝐴 ) )
26	25	ssrdv	⊢ ( ( Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → 𝐷 ⊆ dom 𝐴 )