mapfzcons1

Description: Recover prefix mapping 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	mapfzcons1	$⊢ A \in (B^{(1 \dots N)}) \to {(A \cup \{⟨M, C⟩\}) ↾}_{(1 \dots N)} = A$

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	$⊢ M = N + 1$
2		elmapi	$⊢ A \in (B^{(1 \dots N)}) \to A : (1 \dots N) ⟶ B$
3		ffn	$⊢ A : (1 \dots N) ⟶ B \to A Fn (1 \dots N)$
4		fnresdm	$⊢ A Fn (1 \dots N) \to {A ↾}_{(1 \dots N)} = A$
5	2 3 4	3syl	$⊢ A \in (B^{(1 \dots N)}) \to {A ↾}_{(1 \dots N)} = A$
6	5	uneq1d	$⊢ A \in (B^{(1 \dots N)}) \to ({A ↾}_{(1 \dots N)}) \cup ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = A \cup ({\{⟨M, C⟩\} ↾}_{(1 \dots N)})$
7		resundir	$⊢ {(A \cup \{⟨M, C⟩\}) ↾}_{(1 \dots N)} = ({A ↾}_{(1 \dots N)}) \cup ({\{⟨M, C⟩\} ↾}_{(1 \dots N)})$
8		dmres	$⊢ dom ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = (1 \dots N) \cap dom \{⟨M, C⟩\}$
9		dmsnopss	$⊢ dom \{⟨M, C⟩\} \subseteq \{M\}$
10	1	sneqi	$⊢ \{M\} = \{N + 1\}$
11	9 10	sseqtri	$⊢ dom \{⟨M, C⟩\} \subseteq \{N + 1\}$
12		sslin	$⊢ dom \{⟨M, C⟩\} \subseteq \{N + 1\} \to (1 \dots N) \cap dom \{⟨M, C⟩\} \subseteq (1 \dots N) \cap \{N + 1\}$
13	11 12	ax-mp	$⊢ (1 \dots N) \cap dom \{⟨M, C⟩\} \subseteq (1 \dots N) \cap \{N + 1\}$
14		fzp1disj	$⊢ (1 \dots N) \cap \{N + 1\} = \emptyset$
15		sseq0	$⊢ ((1 \dots N) \cap dom \{⟨M, C⟩\} \subseteq (1 \dots N) \cap \{N + 1\} \land (1 \dots N) \cap \{N + 1\} = \emptyset) \to (1 \dots N) \cap dom \{⟨M, C⟩\} = \emptyset$
16	13 14 15	mp2an	$⊢ (1 \dots N) \cap dom \{⟨M, C⟩\} = \emptyset$
17	8 16	eqtri	$⊢ dom ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = \emptyset$
18		relres	$⊢ Rel ({\{⟨M, C⟩\} ↾}_{(1 \dots N)})$
19		reldm0	$⊢ Rel ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) \to ({\{⟨M, C⟩\} ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = \emptyset)$
20	18 19	ax-mp	$⊢ {\{⟨M, C⟩\} ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = \emptyset$
21	17 20	mpbir	$⊢ {\{⟨M, C⟩\} ↾}_{(1 \dots N)} = \emptyset$
22	21	uneq2i	$⊢ A \cup ({\{⟨M, C⟩\} ↾}_{(1 \dots N)}) = A \cup \emptyset$
23		un0	$⊢ A \cup \emptyset = A$
24	22 23	eqtr2i	$⊢ A = A \cup ({\{⟨M, C⟩\} ↾}_{(1 \dots N)})$
25	6 7 24	3eqtr4g	$⊢ A \in (B^{(1 \dots N)}) \to {(A \cup \{⟨M, C⟩\}) ↾}_{(1 \dots N)} = A$

Metamath Proof Explorer

Theorem mapfzcons1

Proof