Metamath Proof Explorer


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 ) )