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 eluzle 
 |-  ( m e. ( ZZ>= ` N ) -> N <_ m )
32 26 31 syl 
 |-  ( m e. Z -> N <_ m )
33 30 zred 
 |-  ( m e. Z -> m e. RR )
34 leid 
 |-  ( m e. RR -> m <_ m )
35 33 34 syl 
 |-  ( m e. Z -> m <_ m )
36 28 30 30 32 35 elfzd 
 |-  ( m e. Z -> m e. ( N ... m ) )
37 nfcv 
 |-  F/_ n x
38 37 3 nfel 
 |-  F/ n x e. [_ m / n ]_ A
39 4 eleq2d 
 |-  ( n = m -> ( x e. A <-> x e. [_ m / n ]_ A ) )
40 38 39 rspce 
 |-  ( ( m e. ( N ... m ) /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
41 36 40 sylan 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> E. n e. ( N ... m ) x e. A )
42 eliun 
 |-  ( x e. U_ n e. ( N ... m ) A <-> E. n e. ( N ... m ) x e. A )
43 41 42 sylibr 
 |-  ( ( m e. Z /\ x e. [_ m / n ]_ A ) -> x e. U_ n e. ( N ... m ) A )
44 43 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 )
45 24 44 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 )
46 13 15 16 45 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 )
47 46 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 ) ) )
48 11 12 47 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 ) )
49 48 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 ) )
50 10 49 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 )
51 50 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 )
52 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 )
53 51 52 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 )