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