mapfzcons

Description: Extending a one-based mapping by adding a tuple at the end results in another 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	mapfzcons	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to A \cup \{⟨M, C⟩\} \in (B^{(1 \dots M)})$

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	$⊢ M = N + 1$
2		simp2	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to A \in (B^{(1 \dots N)})$
3		elmapex	$⊢ A \in (B^{(1 \dots N)}) \to (B \in V \land (1 \dots N) \in V)$
4	3	simpld	$⊢ A \in (B^{(1 \dots N)}) \to B \in V$
5	4	3ad2ant2	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to B \in V$
6		ovex	$⊢ (1 \dots N) \in V$
7		elmapg	$⊢ (B \in V \land (1 \dots N) \in V) \to (A \in (B^{(1 \dots N)}) \leftrightarrow A : (1 \dots N) ⟶ B)$
8	5 6 7	sylancl	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (A \in (B^{(1 \dots N)}) \leftrightarrow A : (1 \dots N) ⟶ B)$
9	2 8	mpbid	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to A : (1 \dots N) ⟶ B$
10		ovex	$⊢ N + 1 \in V$
11		simp3	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to C \in B$
12		f1osng	$⊢ (N + 1 \in V \land C \in B) \to \{⟨N + 1, C⟩\} : \{N + 1\} \underset{1-1 onto}{⟶} \{C\}$
13	10 11 12	sylancr	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to \{⟨N + 1, C⟩\} : \{N + 1\} \underset{1-1 onto}{⟶} \{C\}$
14		f1of	$⊢ \{⟨N + 1, C⟩\} : \{N + 1\} \underset{1-1 onto}{⟶} \{C\} \to \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ \{C\}$
15	13 14	syl	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ \{C\}$
16		snssi	$⊢ C \in B \to \{C\} \subseteq B$
17	16	3ad2ant3	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to \{C\} \subseteq B$
18	15 17	fssd	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ B$
19		fzp1disj	$⊢ (1 \dots N) \cap \{N + 1\} = \emptyset$
20	19	a1i	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (1 \dots N) \cap \{N + 1\} = \emptyset$
21		fun	$⊢ ((A : (1 \dots N) ⟶ B \land \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ B) \land (1 \dots N) \cap \{N + 1\} = \emptyset) \to (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N) \cup \{N + 1\} ⟶ B \cup B$
22	9 18 20 21	syl21anc	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N) \cup \{N + 1\} ⟶ B \cup B$
23		1z	$⊢ 1 \in ℤ$
24		simp1	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to N \in ℕ_{0}$
25		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
26		1m1e0	$⊢ 1 - 1 = 0$
27	26	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
28	25 27	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
29	24 28	eleqtrdi	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to N \in ℤ_{\geq (1 - 1)}$
30		fzsuc2	$⊢ (1 \in ℤ \land N \in ℤ_{\geq (1 - 1)}) \to (1 \dots N + 1) = (1 \dots N) \cup \{N + 1\}$
31	23 29 30	sylancr	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (1 \dots N + 1) = (1 \dots N) \cup \{N + 1\}$
32	31	eqcomd	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (1 \dots N) \cup \{N + 1\} = (1 \dots N + 1)$
33		unidm	$⊢ B \cup B = B$
34	33	a1i	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to B \cup B = B$
35	32 34	feq23d	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to ((A \cup \{⟨N + 1, C⟩\}) : (1 \dots N) \cup \{N + 1\} ⟶ B \cup B \leftrightarrow (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N + 1) ⟶ B)$
36	22 35	mpbid	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N + 1) ⟶ B$
37		ovex	$⊢ (1 \dots N + 1) \in V$
38		elmapg	$⊢ (B \in V \land (1 \dots N + 1) \in V) \to (A \cup \{⟨N + 1, C⟩\} \in (B^{(1 \dots N + 1)}) \leftrightarrow (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N + 1) ⟶ B)$
39	5 37 38	sylancl	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to (A \cup \{⟨N + 1, C⟩\} \in (B^{(1 \dots N + 1)}) \leftrightarrow (A \cup \{⟨N + 1, C⟩\}) : (1 \dots N + 1) ⟶ B)$
40	36 39	mpbird	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to A \cup \{⟨N + 1, C⟩\} \in (B^{(1 \dots N + 1)})$
41	1	opeq1i	$⊢ ⟨M, C⟩ = ⟨N + 1, C⟩$
42	41	sneqi	$⊢ \{⟨M, C⟩\} = \{⟨N + 1, C⟩\}$
43	42	uneq2i	$⊢ A \cup \{⟨M, C⟩\} = A \cup \{⟨N + 1, C⟩\}$
44	1	oveq2i	$⊢ (1 \dots M) = (1 \dots N + 1)$
45	44	oveq2i	$⊢ B^{(1 \dots M)} = B^{(1 \dots N + 1)}$
46	40 43 45	3eltr4g	$⊢ (N \in ℕ_{0} \land A \in (B^{(1 \dots N)}) \land C \in B) \to A \cup \{⟨M, C⟩\} \in (B^{(1 \dots M)})$

Metamath Proof Explorer

Theorem mapfzcons

Proof