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

Proof

Step	Hyp	Ref	Expression
1		fveqdmss.1	$⊢ D = dom B$
2	1	fveqdmss	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to D \subseteq dom A$
3		dmres	$⊢ dom ({A ↾}_{D}) = D \cap dom A$
4		incom	$⊢ D \cap dom A = dom A \cap D$
5		sseqin2	$⊢ D \subseteq dom A \leftrightarrow dom A \cap D = D$
6	5	biimpi	$⊢ D \subseteq dom A \to dom A \cap D = D$
7	4 6	syl5eq	$⊢ D \subseteq dom A \to D \cap dom A = D$
8	3 7	syl5eq	$⊢ D \subseteq dom A \to dom ({A ↾}_{D}) = D$
9	8 1	syl6eq	$⊢ D \subseteq dom A \to dom ({A ↾}_{D}) = dom B$
10	2 9	syl	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to dom ({A ↾}_{D}) = dom B$
11		fvres	$⊢ x \in D \to ({A ↾}_{D}) (x) = A (x)$
12	11	adantl	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to ({A ↾}_{D}) (x) = A (x)$
13		id	$⊢ A (x) = B (x) \to A (x) = B (x)$
14	12 13	sylan9eq	$⊢ (((Fun B \land \emptyset \notin ran B) \land x \in D) \land A (x) = B (x)) \to ({A ↾}_{D}) (x) = B (x)$
15	14	ex	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to (A (x) = B (x) \to ({A ↾}_{D}) (x) = B (x))$
16	15	ralimdva	$⊢ (Fun B \land \emptyset \notin ran B) \to (\forall x \in D A (x) = B (x) \to \forall x \in D ({A ↾}_{D}) (x) = B (x))$
17	16	3impia	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to \forall x \in D ({A ↾}_{D}) (x) = B (x)$
18	2 7	syl	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to D \cap dom A = D$
19	3 18	syl5eq	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to dom ({A ↾}_{D}) = D$
20	19	raleqdv	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to (\forall x \in dom ({A ↾}_{D}) ({A ↾}_{D}) (x) = B (x) \leftrightarrow \forall x \in D ({A ↾}_{D}) (x) = B (x))$
21	17 20	mpbird	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to \forall x \in dom ({A ↾}_{D}) ({A ↾}_{D}) (x) = B (x)$
22		simpll	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to Fun B$
23	1	eleq2i	$⊢ x \in D \leftrightarrow x \in dom B$
24	23	biimpi	$⊢ x \in D \to x \in dom B$
25	24	adantl	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to x \in dom B$
26		simplr	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to \emptyset \notin ran B$
27		nelrnfvne	$⊢ (Fun B \land x \in dom B \land \emptyset \notin ran B) \to B (x) \neq \emptyset$
28	22 25 26 27	syl3anc	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to B (x) \neq \emptyset$
29		neeq1	$⊢ A (x) = B (x) \to (A (x) \neq \emptyset \leftrightarrow B (x) \neq \emptyset)$
30	28 29	syl5ibrcom	$⊢ ((Fun B \land \emptyset \notin ran B) \land x \in D) \to (A (x) = B (x) \to A (x) \neq \emptyset)$
31	30	ralimdva	$⊢ (Fun B \land \emptyset \notin ran B) \to (\forall x \in D A (x) = B (x) \to \forall x \in D A (x) \neq \emptyset)$
32	31	3impia	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to \forall x \in D A (x) \neq \emptyset$
33		fvn0ssdmfun	$⊢ \forall x \in D A (x) \neq \emptyset \to (D \subseteq dom A \land Fun ({A ↾}_{D}))$
34	33	simprd	$⊢ \forall x \in D A (x) \neq \emptyset \to Fun ({A ↾}_{D})$
35	32 34	syl	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to Fun ({A ↾}_{D})$
36		simp1	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to Fun B$
37		eqfunfv	$⊢ (Fun ({A ↾}_{D}) \land Fun B) \to ({A ↾}_{D} = B \leftrightarrow (dom ({A ↾}_{D}) = dom B \land \forall x \in dom ({A ↾}_{D}) ({A ↾}_{D}) (x) = B (x)))$
38	35 36 37	syl2anc	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to ({A ↾}_{D} = B \leftrightarrow (dom ({A ↾}_{D}) = dom B \land \forall x \in dom ({A ↾}_{D}) ({A ↾}_{D}) (x) = B (x)))$
39	10 21 38	mpbir2and	$⊢ (Fun B \land \emptyset \notin ran B \land \forall x \in D A (x) = B (x)) \to {A ↾}_{D} = B$

Metamath Proof Explorer

Theorem fveqressseq

Proof