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 𝑘 𝐵
iunp1.2 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
iunp1.3 ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion iunp1 ( 𝜑 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴𝐵 ) )

Proof

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 ) ) 𝐴 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴𝐵 ) )