This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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