Theorem iunp1

Description: The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	iunp1.1	$$⊢\underset{\_}{Ⅎ}kB$$
	iunp1.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	iunp1.3	$$⊢k=N+1\to A=B$$
Assertion	iunp1	$$⊢\phi \to \bigcup _{k=M}^{N+1}A=\bigcup _{k=M}^{N}A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		iunp1.1	$$⊢\underset{\_}{Ⅎ}kB$$
2		iunp1.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
3		iunp1.3	$$⊢k=N+1\to A=B$$
4		fzsuc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N+1\right)=\left(M\dots N\right)\cup \left\{N+1\right\}$$
5	2 4	syl	$$⊢\phi \to \left(M\dots N+1\right)=\left(M\dots N\right)\cup \left\{N+1\right\}$$
6	5	iuneq1d	$$⊢\phi \to \bigcup _{k=M}^{N+1}A=\bigcup _{k\in \left(M\dots N\right)\cup \left\{N+1\right\}}A$$
7		iunxun	$$⊢\bigcup _{k\in \left(M\dots N\right)\cup \left\{N+1\right\}}A=\bigcup _{k=M}^{N}A\cup \bigcup _{k\in \left\{N+1\right\}}A$$
8	7	a1i	$$⊢\phi \to \bigcup _{k\in \left(M\dots N\right)\cup \left\{N+1\right\}}A=\bigcup _{k=M}^{N}A\cup \bigcup _{k\in \left\{N+1\right\}}A$$
9		ovex	$$⊢N+1\in \mathrm{V}$$
10	1 9 3	iunxsnf	$$⊢\bigcup _{k\in \left\{N+1\right\}}A=B$$
11	10	a1i	$$⊢\phi \to \bigcup _{k\in \left\{N+1\right\}}A=B$$
12	11	uneq2d	$$⊢\phi \to \bigcup _{k=M}^{N}A\cup \bigcup _{k\in \left\{N+1\right\}}A=\bigcup _{k=M}^{N}A\cup B$$
13	6 8 12	3eqtrd	$$⊢\phi \to \bigcup _{k=M}^{N+1}A=\bigcup _{k=M}^{N}A\cup B$$