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