# Metamath Proof Explorer

## 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}↾}_{{F}\left[\left(0\dots {N}\right)\right]}=\left({{I}↾}_{{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 {ℕ}_{0}$
6 3 5 syl ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
7 elnn0uz ${⊢}{N}\in {ℕ}_{0}↔{N}\in {ℤ}_{\ge 0}$
8 6 7 sylib ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 0}$
9 fzisfzounsn ${⊢}{N}\in {ℤ}_{\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 {F}Fn\left(0..^\left|{F}\right|\right)$
13 fnsnfv ${⊢}\left({F}Fn\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}↾}_{{F}\left[\left(0\dots {N}\right)\right]}={{I}↾}_{\left({F}\left[\left(0..^{N}\right)\right]\cup \left\{{F}\left({N}\right)\right\}\right)}$
18 resundi ${⊢}{{I}↾}_{\left({F}\left[\left(0..^{N}\right)\right]\cup \left\{{F}\left({N}\right)\right\}\right)}=\left({{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left({{I}↾}_{\left\{{F}\left({N}\right)\right\}}\right)$
19 17 18 syl6eq ${⊢}{\phi }\to {{I}↾}_{{F}\left[\left(0\dots {N}\right)\right]}=\left({{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left({{I}↾}_{\left\{{F}\left({N}\right)\right\}}\right)$
20 1 funfnd ${⊢}{\phi }\to {I}Fn\mathrm{dom}{I}$
21 2 3 ffvelrnd ${⊢}{\phi }\to {F}\left({N}\right)\in \mathrm{dom}{I}$
22 fnressn ${⊢}\left({I}Fn\mathrm{dom}{I}\wedge {F}\left({N}\right)\in \mathrm{dom}{I}\right)\to {{I}↾}_{\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}↾}_{\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}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left({{I}↾}_{\left\{{F}\left({N}\right)\right\}}\right)=\left({{I}↾}_{{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}↾}_{{F}\left[\left(0\dots {N}\right)\right]}=\left({{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left\{⟨{F}\left({N}\right),{I}\left({F}\left({N}\right)\right)⟩\right\}$