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 biimpi 
 |-  ( x e. U_ n e. Z A -> E. m e. Z x e. [_ m / n ]_ A )
10 9 adantl 
 |-  ( ( 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 )
11 nfra1 
 |-  F/ m A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B
12 nfv 
 |-  F/ m x e. U_ n e. Z B
13 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 )
14 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 )
15 14 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 )
16 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 )
17 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 )
18 fzssuz 
 |-  ( N ... m ) C_ ( ZZ>= ` N )
19 1 eqcomi 
 |-  ( ZZ>= ` N ) = Z
20 18 19 sseqtri 
 |-  ( N ... m ) C_ Z
21 iunss1 
 |-  ( ( N ... m ) C_ Z -> U_ n e. ( N ... m ) B C_ U_ n e. Z B )
22 20 21 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 )
23 17 22 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 )
24 23 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 )
25 1 eleq2i 
 |-  ( m e. Z <-> m e. ( ZZ>= ` N ) )
26 25 biimpi 
 |-  ( m e. Z -> m e. ( ZZ>= ` N ) )
27 eluzel2 
 |-  ( m e. ( ZZ>= ` N ) -> N e. ZZ )
28 26 27 syl 
 |-  ( m e. Z -> N e. ZZ )
29 eluzelz 
 |-  ( m e. ( ZZ>= ` N ) -> m e. ZZ )
30 26 29 syl 
 |-  ( m e. Z -> m e. ZZ )
31 28 30 30 3jca 
 |-  ( m e. Z -> ( N e. ZZ /\ m e. ZZ /\ m e. ZZ ) )
32 eluzle 
 |-  ( m e. ( ZZ>= ` N ) -> N <_ m )
33 26 32 syl 
 |-  ( m e. Z -> N <_ m )
34 30 zred 
 |-  ( m e. Z -> m e. RR )
35 leid 
 |-  ( m e. RR -> m <_ m )
36 34 35 syl 
 |-  ( m e. Z -> m <_ m )
37 31 33 36 jca32 
 |-  ( m e. Z -> ( ( N e. ZZ /\ m e. ZZ /\ m e. ZZ ) /\ ( N <_ m /\ m <_ m ) ) )
38 elfz2 
 |-  ( m e. ( N ... m ) <-> ( ( N e. ZZ /\ m e. ZZ /\ m e. ZZ ) /\ ( N <_ m /\ m <_ m ) ) )
39 37 38 sylibr 
 |-  ( m e. Z -> m e. ( N ... m ) )
40 nfcv 
 |-  F/_ n x
41 40 3 nfel 
 |-  F/ n x e. [_ m / n ]_ A
42 4 eleq2d 
 |-  ( n = m -> ( x e. A <-> x e. [_ m / n ]_ A ) )
43 41 42 rspce 
 |-  ( ( m e. ( N ... m ) /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
44 39 43 sylan 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
45 eliun 
 |-  ( x e. U_ n e. ( N ... m ) A <-> E. n e. ( N ... m ) x e. A )
46 44 45 sylibr 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. ( N ... m ) A )
47 46 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 )
48 24 47 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 )
49 13 15 16 48 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 )
50 49 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 ) ) )
51 11 12 50 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 ) )
52 51 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 ) )
53 10 52 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 )
54 53 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 )
55 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 )
56 54 55 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 )