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