Step |
Hyp |
Ref |
Expression |
1 |
|
iunp1.1 |
⊢ Ⅎ 𝑘 𝐵 |
2 |
|
iunp1.2 |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
3 |
|
iunp1.3 |
⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 ) |
4 |
|
fzsuc |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ) |
5 |
2 4
|
syl |
⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ) |
6 |
5
|
iuneq1d |
⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ∪ 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) 𝐴 ) |
7 |
|
iunxun |
⊢ ∪ 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) 𝐴 = ( ∪ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∪ ∪ 𝑘 ∈ { ( 𝑁 + 1 ) } 𝐴 ) |
8 |
7
|
a1i |
⊢ ( 𝜑 → ∪ 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) 𝐴 = ( ∪ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∪ ∪ 𝑘 ∈ { ( 𝑁 + 1 ) } 𝐴 ) ) |
9 |
|
ovex |
⊢ ( 𝑁 + 1 ) ∈ V |
10 |
1 9 3
|
iunxsnf |
⊢ ∪ 𝑘 ∈ { ( 𝑁 + 1 ) } 𝐴 = 𝐵 |
11 |
10
|
a1i |
⊢ ( 𝜑 → ∪ 𝑘 ∈ { ( 𝑁 + 1 ) } 𝐴 = 𝐵 ) |
12 |
11
|
uneq2d |
⊢ ( 𝜑 → ( ∪ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∪ ∪ 𝑘 ∈ { ( 𝑁 + 1 ) } 𝐴 ) = ( ∪ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∪ 𝐵 ) ) |
13 |
6 8 12
|
3eqtrd |
⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∪ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∪ 𝐵 ) ) |