This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iuneqfzuz

Description: If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis iuneqfzuz.z ⊢ Z = ℤ ≥ N
Assertion iuneqfzuz ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B → ⋃ n ∈ Z A = ⋃ n ∈ Z B

Proof

Step Hyp Ref Expression
1 iuneqfzuz.z ⊢ Z = ℤ ≥ N
2 1 iuneqfzuzlem ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B → ⋃ n ∈ Z A ⊆ ⋃ n ∈ Z B
3 eqcom ⊢ ⋃ n = N m A = ⋃ n = N m B ↔ ⋃ n = N m B = ⋃ n = N m A
4 3 ralbii ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B ↔ ∀ m ∈ Z ⋃ n = N m B = ⋃ n = N m A
5 4 biimpi ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B → ∀ m ∈ Z ⋃ n = N m B = ⋃ n = N m A
6 1 iuneqfzuzlem ⊢ ∀ m ∈ Z ⋃ n = N m B = ⋃ n = N m A → ⋃ n ∈ Z B ⊆ ⋃ n ∈ Z A
7 5 6 syl ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B → ⋃ n ∈ Z B ⊆ ⋃ n ∈ Z A
8 2 7 eqssd ⊢ ∀ m ∈ Z ⋃ n = N m A = ⋃ n = N m B → ⋃ n ∈ Z A = ⋃ n ∈ Z B