Theorem 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 \left(B^{\left(1\dots N\right)}\right)\to {\left(A\cup \left\{⟨M,C⟩\right\}\right)\upharpoonright }_{\left(1\dots N\right)}=A$$

Proof

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