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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
Assertion iuneqfzuz ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 = ∪ 𝑛 ∈ 𝑍 𝐵 )

Proof

Step Hyp Ref Expression
1 iuneqfzuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
2 1 iuneqfzuzlem ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 ⊆ ∪ 𝑛 ∈ 𝑍 𝐵 )
3 eqcom ⊢ ( ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ↔ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
4 3 ralbii ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 ↔ ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
5 4 biimpi ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 )
6 1 iuneqfzuzlem ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 → ∪ 𝑛 ∈ 𝑍 𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐴 )
7 5 6 syl ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐵 ⊆ ∪ 𝑛 ∈ 𝑍 𝐴 )
8 2 7 eqssd ⊢ ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐴 = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) 𝐵 → ∪ 𝑛 ∈ 𝑍 𝐴 = ∪ 𝑛 ∈ 𝑍 𝐵 )