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 ⊢ Ⅎ _ k B
iunp1.2 ⊢ φ → N ∈ ℤ ≥ M
iunp1.3 ⊢ k = N + 1 → A = B
Assertion iunp1 ⊢ φ → ⋃ k = M N + 1 A = ⋃ k = M N A ∪ B

Proof

Step Hyp Ref Expression
1 iunp1.1 ⊢ Ⅎ _ k B
2 iunp1.2 ⊢ φ → N ∈ ℤ ≥ M
3 iunp1.3 ⊢ k = N + 1 → A = B
4 fzsuc ⊢ N ∈ ℤ ≥ M → M … N + 1 = M … N ∪ N + 1
5 2 4 syl ⊢ φ → M … N + 1 = M … N ∪ N + 1
6 5 iuneq1d ⊢ φ → ⋃ k = M N + 1 A = ⋃ k ∈ M … N ∪ N + 1 A
7 iunxun ⊢ ⋃ k ∈ M … N ∪ N + 1 A = ⋃ k = M N A ∪ ⋃ k ∈ N + 1 A
8 7 a1i ⊢ φ → ⋃ k ∈ M … N ∪ N + 1 A = ⋃ k = M N A ∪ ⋃ k ∈ N + 1 A
9 ovex ⊢ N + 1 ∈ V
10 1 9 3 iunxsnf ⊢ ⋃ k ∈ N + 1 A = B
11 10 a1i ⊢ φ → ⋃ k ∈ N + 1 A = B
12 11 uneq2d ⊢ φ → ⋃ k = M N A ∪ ⋃ k ∈ N + 1 A = ⋃ k = M N A ∪ B
13 6 8 12 3eqtrd ⊢ φ → ⋃ k = M N + 1 A = ⋃ k = M N A ∪ B