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