mapfzcons2

Description: Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

		Ref	Expression
	Hypothesis	mapfzcons.1	$⊢ M = N + 1$
	Assertion	mapfzcons2	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to (A \cup \{⟨M, C⟩\}) (M) = C$

Step	Hyp	Ref	Expression
1		mapfzcons.1	$⊢ M = N + 1$
2		ovex	$⊢ N + 1 \in V$
3	1 2	eqeltri	$⊢ M \in V$
4	3	a1i	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to M \in V$
5		elex	$⊢ C \in B \to C \in V$
6	5	adantl	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to C \in V$
7		elmapi	$⊢ A \in (B^{(1 \dots N)}) \to A : (1 \dots N) ⟶ B$
8	7	fdmd	$⊢ A \in (B^{(1 \dots N)}) \to dom A = (1 \dots N)$
9	8	adantr	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to dom A = (1 \dots N)$
10	9	ineq1d	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to dom A \cap \{M\} = (1 \dots N) \cap \{M\}$
11	1	sneqi	$⊢ \{M\} = \{N + 1\}$
12	11	ineq2i	$⊢ (1 \dots N) \cap \{M\} = (1 \dots N) \cap \{N + 1\}$
13		fzp1disj	$⊢ (1 \dots N) \cap \{N + 1\} = \emptyset$
14	12 13	eqtri	$⊢ (1 \dots N) \cap \{M\} = \emptyset$
15	10 14	eqtrdi	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to dom A \cap \{M\} = \emptyset$
16		disjsn	$⊢ dom A \cap \{M\} = \emptyset \leftrightarrow \neg M \in dom A$
17	15 16	sylib	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to \neg M \in dom A$
18		fsnunfv	$⊢ (M \in V \land C \in V \land \neg M \in dom A) \to (A \cup \{⟨M, C⟩\}) (M) = C$
19	4 6 17 18	syl3anc	$⊢ (A \in (B^{(1 \dots N)}) \land C \in B) \to (A \cup \{⟨M, C⟩\}) (M) = C$

Metamath Proof Explorer