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	|- F/_ k B
	iunp1.2	|- ( ph -> N e. ( ZZ>= ` M ) )
	iunp1.3	|- ( k = ( N + 1 ) -> A = B )
Assertion	iunp1	|- ( ph -> U_ k e. ( M ... ( N + 1 ) ) A = ( U_ k e. ( M ... N ) A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		iunp1.1	|- F/_ k B
2		iunp1.2	|- ( ph -> N e. ( ZZ>= ` M ) )
3		iunp1.3	|- ( k = ( N + 1 ) -> A = B )
4		fzsuc	|- ( N e. ( ZZ>= ` M ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
5	2 4	syl	|- ( ph -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
6	5	iuneq1d	|- ( ph -> U_ k e. ( M ... ( N + 1 ) ) A = U_ k e. ( ( M ... N ) u. { ( N + 1 ) } ) A )
7		iunxun	|- U_ k e. ( ( M ... N ) u. { ( N + 1 ) } ) A = ( U_ k e. ( M ... N ) A u. U_ k e. { ( N + 1 ) } A )
8	7	a1i	|- ( ph -> U_ k e. ( ( M ... N ) u. { ( N + 1 ) } ) A = ( U_ k e. ( M ... N ) A u. U_ k e. { ( N + 1 ) } A ) )
9		ovex	|- ( N + 1 ) e. _V
10	1 9 3	iunxsnf	|- U_ k e. { ( N + 1 ) } A = B
11	10	a1i	|- ( ph -> U_ k e. { ( N + 1 ) } A = B )
12	11	uneq2d	|- ( ph -> ( U_ k e. ( M ... N ) A u. U_ k e. { ( N + 1 ) } A ) = ( U_ k e. ( M ... N ) A u. B ) )
13	6 8 12	3eqtrd	|- ( ph -> U_ k e. ( M ... ( N + 1 ) ) A = ( U_ k e. ( M ... N ) A u. B ) )