fvmpti

Description: Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

Step	Hyp	Ref	Expression
1		fvmptg.1	$⊢ x = A \to B = C$
2		fvmptg.2	$⊢ F = (x \in D ⟼ B)$
3	1 2	fvmptg	$⊢ (A \in D \land C \in V) \to F (A) = C$
4		fvi	$⊢ C \in V \to I (C) = C$
5	4	adantl	$⊢ (A \in D \land C \in V) \to I (C) = C$
6	3 5	eqtr4d	$⊢ (A \in D \land C \in V) \to F (A) = I (C)$
7	1	eleq1d	$⊢ x = A \to (B \in V \leftrightarrow C \in V)$
8	2	dmmpt	$⊢ dom F = \{x \in D \| B \in V\}$
9	7 8	elrab2	$⊢ A \in dom F \leftrightarrow (A \in D \land C \in V)$
10	9	baib	$⊢ A \in D \to (A \in dom F \leftrightarrow C \in V)$
11	10	notbid	$⊢ A \in D \to (\neg A \in dom F \leftrightarrow \neg C \in V)$
12		ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$
13	11 12	syl6bir	$⊢ A \in D \to (\neg C \in V \to F (A) = \emptyset)$
14	13	imp	$⊢ (A \in D \land \neg C \in V) \to F (A) = \emptyset$
15		fvprc	$⊢ \neg C \in V \to I (C) = \emptyset$
16	15	adantl	$⊢ (A \in D \land \neg C \in V) \to I (C) = \emptyset$
17	14 16	eqtr4d	$⊢ (A \in D \land \neg C \in V) \to F (A) = I (C)$
18	6 17	pm2.61dan	$⊢ A \in D \to F (A) = I (C)$

Metamath Proof Explorer