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 = ( ZZ>= ` N )
Assertion iuneqfzuz 
|- ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A = U_ n e. Z B )

Proof

Step Hyp Ref Expression
1 iuneqfzuz.z 
 |-  Z = ( ZZ>= ` N )
2 1 iuneqfzuzlem 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A C_ U_ n e. Z B )
3 eqcom 
 |-  ( U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B <-> U_ n e. ( N ... m ) B = U_ n e. ( N ... m ) A )
4 3 ralbii 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B <-> A. m e. Z U_ n e. ( N ... m ) B = U_ n e. ( N ... m ) A )
5 4 biimpi 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> A. m e. Z U_ n e. ( N ... m ) B = U_ n e. ( N ... m ) A )
6 1 iuneqfzuzlem 
 |-  ( A. m e. Z U_ n e. ( N ... m ) B = U_ n e. ( N ... m ) A -> U_ n e. Z B C_ U_ n e. Z A )
7 5 6 syl 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z B C_ U_ n e. Z A )
8 2 7 eqssd 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A = U_ n e. Z B )