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	$⊢ D = dom B$
	Assertion	fveqdmss	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to D \subseteq dom A$

Proof

Step	Hyp	Ref	Expression
1		fveqdmss.1	$⊢ D = dom B$
2		fveq2	$⊢ x = a \to A (x) = A (a)$
3		fveq2	$⊢ x = a \to B (x) = B (a)$
4	2 3	eqeq12d	$⊢ x = a \to (A (x) = B (x) \leftrightarrow A (a) = B (a))$
5	4	rspcva	$⊢ (a \in D \land \forall x \in D A (x) = B (x)) \to A (a) = B (a)$
6		nelrnfvne	$⊢ (Fun B \land a \in dom B \land \emptyset \notin ran B) \to B (a) \neq \emptyset$
7		n0	$⊢ B (a) \neq \emptyset \leftrightarrow \exists b b \in B (a)$
8		eleq2	$⊢ B (a) = A (a) \to (b \in B (a) \leftrightarrow b \in A (a))$
9	8	eqcoms	$⊢ A (a) = B (a) \to (b \in B (a) \leftrightarrow b \in A (a))$
10		elfvdm	$⊢ b \in A (a) \to a \in dom A$
11	9 10	biimtrdi	$⊢ A (a) = B (a) \to (b \in B (a) \to a \in dom A)$
12	11	com12	$⊢ b \in B (a) \to (A (a) = B (a) \to a \in dom A)$
13	12	exlimiv	$⊢ \exists b b \in B (a) \to (A (a) = B (a) \to a \in dom A)$
14	7 13	sylbi	$⊢ B (a) \neq \emptyset \to (A (a) = B (a) \to a \in dom A)$
15	6 14	syl	$⊢ (Fun B \land a \in dom B \land \emptyset \notin ran B) \to (A (a) = B (a) \to a \in dom A)$
16	15	3exp	$⊢ Fun B \to (a \in dom B \to (\emptyset \notin ran B \to (A (a) = B (a) \to a \in dom A)))$
17	16	com12	$⊢ a \in dom B \to (Fun B \to (\emptyset \notin ran B \to (A (a) = B (a) \to a \in dom A)))$
18	17 1	eleq2s	$⊢ a \in D \to (Fun B \to (\emptyset \notin ran B \to (A (a) = B (a) \to a \in dom A)))$
19	18	com24	$⊢ a \in D \to (A (a) = B (a) \to (\emptyset \notin ran B \to (Fun B \to a \in dom A)))$
20	19	adantr	$⊢ (a \in D \land \forall x \in D A (x) = B (x)) \to (A (a) = B (a) \to (\emptyset \notin ran B \to (Fun B \to a \in dom A)))$
21	5 20	mpd	$⊢ (a \in D \land \forall x \in D A (x) = B (x)) \to (\emptyset \notin ran B \to (Fun B \to a \in dom A))$
22	21	ex	$⊢ a \in D \to (\forall x \in D A (x) = B (x) \to (\emptyset \notin ran B \to (Fun B \to a \in dom A)))$
23	22	com23	$⊢ a \in D \to (\emptyset \notin ran B \to (\forall x \in D A (x) = B (x) \to (Fun B \to a \in dom A)))$
24	23	com14	$⊢ Fun B \to (\emptyset \notin ran B \to (\forall x \in D A (x) = B (x) \to (a \in D \to a \in dom A)))$
25	24	3imp	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to (a \in D \to a \in dom A)$
26	25	ssrdv	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to D \subseteq dom A$

Metamath Proof Explorer

Theorem fveqdmss

Proof