Metamath Proof Explorer

Theorem iuneqfzuzlem

Description: Lemma for iuneqfzuz : here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis iuneqfzuzlem.z 
|- Z = ( ZZ>= ` N )
Assertion 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 )

Proof

Step Hyp Ref Expression
1 iuneqfzuzlem.z 
 |-  Z = ( ZZ>= ` N )
2 nfcv 
 |-  F/_ m A
3 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
4 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
5 2 3 4 cbviun 
 |-  U_ n e. Z A = U_ m e. Z [_ m / n ]_ A
6 5 eleq2i 
 |-  ( x e. U_ n e. Z A <-> x e. U_ m e. Z [_ m / n ]_ A )
7 eliun 
 |-  ( x e. U_ m e. Z [_ m / n ]_ A <-> E. m e. Z x e. [_ m / n ]_ A )
8 6 7 bitri 
 |-  ( x e. U_ n e. Z A <-> E. m e. Z x e. [_ m / n ]_ A )
9 8 bilani 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. U_ n e. Z A ) -> E. m e. Z x e. [_ m / n ]_ A )
10 nfra1 
 |-  F/ m A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B
11 nfv 
 |-  F/ m x e. U_ n e. Z B
12 simp2 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ m e. Z /\ x e. [_ m / n ]_ A ) -> m e. Z )
13 rspa 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ m e. Z ) -> U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B )
14 13 3adant3 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ m e. Z /\ x e. [_ m / n ]_ A ) -> U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B )
15 simp3 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ m e. Z /\ x e. [_ m / n ]_ A ) -> x e. [_ m / n ]_ A )
16 id 
 |-  ( U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B )
17 fzssuz 
 |-  ( N ... m ) C_ ( ZZ>= ` N )
18 1 eqcomi 
 |-  ( ZZ>= ` N ) = Z
19 17 18 sseqtri 
 |-  ( N ... m ) C_ Z
20 iunss1 
 |-  ( ( N ... m ) C_ Z -> U_ n e. ( N ... m ) B C_ U_ n e. Z B )
21 19 20 mp1i 
 |-  ( U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. ( N ... m ) B C_ U_ n e. Z B )
22 16 21 eqsstrd 
 |-  ( U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. ( N ... m ) A C_ U_ n e. Z B )
23 22 3ad2ant2 
 |-  ( ( m e. Z /\ U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. [_ m / n ]_ A ) -> U_ n e. ( N ... m ) A C_ U_ n e. Z B )
24 1 eleq2i 
 |-  ( m e. Z <-> m e. ( ZZ>= ` N ) )
25 24 biimpi 
 |-  ( m e. Z -> m e. ( ZZ>= ` N ) )
26 eluzel2 
 |-  ( m e. ( ZZ>= ` N ) -> N e. ZZ )
27 25 26 syl 
 |-  ( m e. Z -> N e. ZZ )
28 eluzelz 
 |-  ( m e. ( ZZ>= ` N ) -> m e. ZZ )
29 25 28 syl 
 |-  ( m e. Z -> m e. ZZ )
30 eluzle 
 |-  ( m e. ( ZZ>= ` N ) -> N <_ m )
31 25 30 syl 
 |-  ( m e. Z -> N <_ m )
32 29 zred 
 |-  ( m e. Z -> m e. RR )
33 leid 
 |-  ( m e. RR -> m <_ m )
34 32 33 syl 
 |-  ( m e. Z -> m <_ m )
35 27 29 29 31 34 elfzd 
 |-  ( m e. Z -> m e. ( N ... m ) )
36 nfcv 
 |-  F/_ n x
37 36 3 nfel 
 |-  F/ n x e. [_ m / n ]_ A
38 4 eleq2d 
 |-  ( n = m -> ( x e. A <-> x e. [_ m / n ]_ A ) )
39 37 38 rspce 
 |-  ( ( m e. ( N ... m ) /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
40 35 39 sylan 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
41 eliun 
 |-  ( x e. U_ n e. ( N ... m ) A <-> E. n e. ( N ... m ) x e. A )
42 40 41 sylibr 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. ( N ... m ) A )
43 42 3adant2 
 |-  ( ( m e. Z /\ U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. ( N ... m ) A )
44 23 43 sseldd 
 |-  ( ( m e. Z /\ U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. Z B )
45 12 14 15 44 syl3anc 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ m e. Z /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. Z B )
46 45 3exp 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> ( m e. Z -> ( x e. [_ m / n ]_ A -> x e. U_ n e. Z B ) ) )
47 10 11 46 rexlimd 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> ( E. m e. Z x e. [_ m / n ]_ A -> x e. U_ n e. Z B ) )
48 47 adantr 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. U_ n e. Z A ) -> ( E. m e. Z x e. [_ m / n ]_ A -> x e. U_ n e. Z B ) )
49 9 48 mpd 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B /\ x e. U_ n e. Z A ) -> x e. U_ n e. Z B )
50 49 ralrimiva 
 |-  ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> A. x e. U_ n e. Z A x e. U_ n e. Z B )
51 dfss3 
 |-  ( U_ n e. Z A C_ U_ n e. Z B <-> A. x e. U_ n e. Z A x e. U_ n e. Z B )
52 50 51 sylibr 
 |-  ( 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 )