Theorem resunimafz0

Description: TODO-AV: Revise using F e. Word dom I ? Formerly part of proof of eupth2lem3 : The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

	Ref	Expression
Hypotheses	resunimafz0.i	$$⊢\phi \to \mathrm{Fun}I$$
	resunimafz0.f	$$⊢\phi \to F:\left(0..^\left|F\right|\right)⟶\mathrm{dom}I$$
	resunimafz0.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
Assertion	resunimafz0	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}=\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		resunimafz0.i	$$⊢\phi \to \mathrm{Fun}I$$
2		resunimafz0.f	$$⊢\phi \to F:\left(0..^\left|F\right|\right)⟶\mathrm{dom}I$$
3		resunimafz0.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
4		imaundi	$$⊢F\left[\left(0..^N\right)\cup \left\{N\right\}\right]=F\left[\left(0..^N\right)\right]\cup F\left[\left\{N\right\}\right]$$
5		elfzonn0	$$⊢N\in \left(0..^\left|F\right|\right)\to N\in {\mathbb{N}}_0$$
6	3 5	syl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
8	6 7	sylib	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 0}$$
9		fzisfzounsn	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left(0\dots N\right)=\left(0..^N\right)\cup \left\{N\right\}$$
10	8 9	syl	$$⊢\phi \to \left(0\dots N\right)=\left(0..^N\right)\cup \left\{N\right\}$$
11	10	imaeq2d	$$⊢\phi \to F\left[\left(0\dots N\right)\right]=F\left[\left(0..^N\right)\cup \left\{N\right\}\right]$$
12	2	ffnd	$$⊢\phi \to FFn\left(0..^\left|F\right|\right)$$
13		fnsnfv	$$⊢\left(FFn\left(0..^\left|F\right|\right)\wedge N\in \left(0..^\left|F\right|\right)\right)\to \left\{F\left(N\right)\right\}=F\left[\left\{N\right\}\right]$$
14	12 3 13	syl2anc	$$⊢\phi \to \left\{F\left(N\right)\right\}=F\left[\left\{N\right\}\right]$$
15	14	uneq2d	$$⊢\phi \to F\left[\left(0..^N\right)\right]\cup \left\{F\left(N\right)\right\}=F\left[\left(0..^N\right)\right]\cup F\left[\left\{N\right\}\right]$$
16	4 11 15	3eqtr4a	$$⊢\phi \to F\left[\left(0\dots N\right)\right]=F\left[\left(0..^N\right)\right]\cup \left\{F\left(N\right)\right\}$$
17	16	reseq2d	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}={I\upharpoonright }_{\left(F\left[\left(0..^N\right)\right]\cup \left\{F\left(N\right)\right\}\right)}$$
18		resundi	$$⊢{I\upharpoonright }_{\left(F\left[\left(0..^N\right)\right]\cup \left\{F\left(N\right)\right\}\right)}=\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left({I\upharpoonright }_{\left\{F\left(N\right)\right\}}\right)$$
19	17 18	eqtrdi	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}=\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left({I\upharpoonright }_{\left\{F\left(N\right)\right\}}\right)$$
20	1	funfnd	$$⊢\phi \to IFn\mathrm{dom}I$$
21	2 3	ffvelrnd	$$⊢\phi \to F\left(N\right)\in \mathrm{dom}I$$
22		fnressn	$$⊢\left(IFn\mathrm{dom}I\wedge F\left(N\right)\in \mathrm{dom}I\right)\to {I\upharpoonright }_{\left\{F\left(N\right)\right\}}=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
23	20 21 22	syl2anc	$$⊢\phi \to {I\upharpoonright }_{\left\{F\left(N\right)\right\}}=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
24	23	uneq2d	$$⊢\phi \to \left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left({I\upharpoonright }_{\left\{F\left(N\right)\right\}}\right)=\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
25	19 24	eqtrd	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}=\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\cup \left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$