Metamath Proof Explorer

Theorem fzisoeu

Description: A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fzisoeu.h 
|- ( ph -> H e. Fin )
fzisoeu.or 
|- ( ph -> < Or H )
fzisoeu.m 
|- ( ph -> M e. ZZ )
fzisoeu.4 
|- N = ( ( # ` H ) + ( M - 1 ) )
Assertion fzisoeu 
|- ( ph -> E! f f Isom < , < ( ( M ... N ) , H ) )

Proof

Step Hyp Ref Expression
1 fzisoeu.h 
 |-  ( ph -> H e. Fin )
2 fzisoeu.or 
 |-  ( ph -> < Or H )
3 fzisoeu.m 
 |-  ( ph -> M e. ZZ )
4 fzisoeu.4 
 |-  N = ( ( # ` H ) + ( M - 1 ) )
5 fzssz 
 |-  ( M ... N ) C_ ZZ
6 zssre 
 |-  ZZ C_ RR
7 5 6 sstri 
 |-  ( M ... N ) C_ RR
8 ltso 
 |-  < Or RR
9 soss 
 |-  ( ( M ... N ) C_ RR -> ( < Or RR -> < Or ( M ... N ) ) )
10 7 8 9 mp2 
 |-  < Or ( M ... N )
11 fzfi 
 |-  ( M ... N ) e. Fin
12 fz1iso 
 |-  ( ( < Or ( M ... N ) /\ ( M ... N ) e. Fin ) -> E. h h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) )
13 10 11 12 mp2an 
 |-  E. h h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) )
14 fveq2 
 |-  ( H = (/) -> ( # ` H ) = ( # ` (/) ) )
15 hash0 
 |-  ( # ` (/) ) = 0
16 14 15 eqtrdi 
 |-  ( H = (/) -> ( # ` H ) = 0 )
17 16 oveq1d 
 |-  ( H = (/) -> ( ( # ` H ) + ( M - 1 ) ) = ( 0 + ( M - 1 ) ) )
18 4 17 eqtrid 
 |-  ( H = (/) -> N = ( 0 + ( M - 1 ) ) )
19 18 oveq2d 
 |-  ( H = (/) -> ( M ... N ) = ( M ... ( 0 + ( M - 1 ) ) ) )
20 19 adantl 
 |-  ( ( ph /\ H = (/) ) -> ( M ... N ) = ( M ... ( 0 + ( M - 1 ) ) ) )
21 3 zcnd 
 |-  ( ph -> M e. CC )
22 1cnd 
 |-  ( ph -> 1 e. CC )
23 21 22 subcld 
 |-  ( ph -> ( M - 1 ) e. CC )
24 23 addid2d 
 |-  ( ph -> ( 0 + ( M - 1 ) ) = ( M - 1 ) )
25 24 oveq2d 
 |-  ( ph -> ( M ... ( 0 + ( M - 1 ) ) ) = ( M ... ( M - 1 ) ) )
26 3 zred 
 |-  ( ph -> M e. RR )
27 26 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
28 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
29 3 28 syl 
 |-  ( ph -> ( M - 1 ) e. ZZ )
30 fzn 
 |-  ( ( M e. ZZ /\ ( M - 1 ) e. ZZ ) -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
31 3 29 30 syl2anc 
 |-  ( ph -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
32 27 31 mpbid 
 |-  ( ph -> ( M ... ( M - 1 ) ) = (/) )
33 25 32 eqtrd 
 |-  ( ph -> ( M ... ( 0 + ( M - 1 ) ) ) = (/) )
34 33 adantr 
 |-  ( ( ph /\ H = (/) ) -> ( M ... ( 0 + ( M - 1 ) ) ) = (/) )
35 eqcom 
 |-  ( H = (/) <-> (/) = H )
36 35 biimpi 
 |-  ( H = (/) -> (/) = H )
37 36 adantl 
 |-  ( ( ph /\ H = (/) ) -> (/) = H )
38 20 34 37 3eqtrd 
 |-  ( ( ph /\ H = (/) ) -> ( M ... N ) = H )
39 38 fveq2d 
 |-  ( ( ph /\ H = (/) ) -> ( # ` ( M ... N ) ) = ( # ` H ) )
40 22 21 pncan3d 
 |-  ( ph -> ( 1 + ( M - 1 ) ) = M )
41 40 eqcomd 
 |-  ( ph -> M = ( 1 + ( M - 1 ) ) )
42 41 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> M = ( 1 + ( M - 1 ) ) )
43 1red 
 |-  ( ( ph /\ -. H = (/) ) -> 1 e. RR )
44 neqne 
 |-  ( -. H = (/) -> H =/= (/) )
45 44 adantl 
 |-  ( ( ph /\ -. H = (/) ) -> H =/= (/) )
46 1 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> H e. Fin )
47 hashnncl 
 |-  ( H e. Fin -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
48 46 47 syl 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
49 45 48 mpbird 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` H ) e. NN )
50 49 nnred 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` H ) e. RR )
51 29 zred 
 |-  ( ph -> ( M - 1 ) e. RR )
52 51 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( M - 1 ) e. RR )
53 49 nnge1d 
 |-  ( ( ph /\ -. H = (/) ) -> 1 <_ ( # ` H ) )
54 43 50 52 53 leadd1dd 
 |-  ( ( ph /\ -. H = (/) ) -> ( 1 + ( M - 1 ) ) <_ ( ( # ` H ) + ( M - 1 ) ) )
55 54 4 breqtrrdi 
 |-  ( ( ph /\ -. H = (/) ) -> ( 1 + ( M - 1 ) ) <_ N )
56 42 55 eqbrtrd 
 |-  ( ( ph /\ -. H = (/) ) -> M <_ N )
57 3 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> M e. ZZ )
58 hashcl 
 |-  ( H e. Fin -> ( # ` H ) e. NN0 )
59 nn0z 
 |-  ( ( # ` H ) e. NN0 -> ( # ` H ) e. ZZ )
60 1 58 59 3syl 
 |-  ( ph -> ( # ` H ) e. ZZ )
61 60 29 zaddcld 
 |-  ( ph -> ( ( # ` H ) + ( M - 1 ) ) e. ZZ )
62 4 61 eqeltrid 
 |-  ( ph -> N e. ZZ )
63 62 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> N e. ZZ )
64 eluz 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
65 57 63 64 syl2anc 
 |-  ( ( ph /\ -. H = (/) ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
66 56 65 mpbird 
 |-  ( ( ph /\ -. H = (/) ) -> N e. ( ZZ>= ` M ) )
67 hashfz 
 |-  ( N e. ( ZZ>= ` M ) -> ( # ` ( M ... N ) ) = ( ( N - M ) + 1 ) )
68 66 67 syl 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` ( M ... N ) ) = ( ( N - M ) + 1 ) )
69 4 oveq1i 
 |-  ( N - M ) = ( ( ( # ` H ) + ( M - 1 ) ) - M )
70 1 58 syl 
 |-  ( ph -> ( # ` H ) e. NN0 )
71 70 nn0cnd 
 |-  ( ph -> ( # ` H ) e. CC )
72 71 23 21 addsubassd 
 |-  ( ph -> ( ( ( # ` H ) + ( M - 1 ) ) - M ) = ( ( # ` H ) + ( ( M - 1 ) - M ) ) )
73 69 72 eqtrid 
 |-  ( ph -> ( N - M ) = ( ( # ` H ) + ( ( M - 1 ) - M ) ) )
74 22 negcld 
 |-  ( ph -> -u 1 e. CC )
75 21 22 negsubd 
 |-  ( ph -> ( M + -u 1 ) = ( M - 1 ) )
76 75 eqcomd 
 |-  ( ph -> ( M - 1 ) = ( M + -u 1 ) )
77 21 74 76 mvrladdd 
 |-  ( ph -> ( ( M - 1 ) - M ) = -u 1 )
78 77 oveq2d 
 |-  ( ph -> ( ( # ` H ) + ( ( M - 1 ) - M ) ) = ( ( # ` H ) + -u 1 ) )
79 73 78 eqtrd 
 |-  ( ph -> ( N - M ) = ( ( # ` H ) + -u 1 ) )
80 79 oveq1d 
 |-  ( ph -> ( ( N - M ) + 1 ) = ( ( ( # ` H ) + -u 1 ) + 1 ) )
81 80 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( N - M ) + 1 ) = ( ( ( # ` H ) + -u 1 ) + 1 ) )
82 71 22 negsubd 
 |-  ( ph -> ( ( # ` H ) + -u 1 ) = ( ( # ` H ) - 1 ) )
83 82 oveq1d 
 |-  ( ph -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( ( ( # ` H ) - 1 ) + 1 ) )
84 71 22 npcand 
 |-  ( ph -> ( ( ( # ` H ) - 1 ) + 1 ) = ( # ` H ) )
85 83 84 eqtrd 
 |-  ( ph -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( # ` H ) )
86 85 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( # ` H ) )
87 68 81 86 3eqtrd 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` ( M ... N ) ) = ( # ` H ) )
88 39 87 pm2.61dan 
 |-  ( ph -> ( # ` ( M ... N ) ) = ( # ` H ) )
89 88 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` ( M ... N ) ) ) = ( 1 ... ( # ` H ) ) )
90 isoeq4 
 |-  ( ( 1 ... ( # ` ( M ... N ) ) ) = ( 1 ... ( # ` H ) ) -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) <-> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
91 89 90 syl 
 |-  ( ph -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) <-> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
92 91 biimpd 
 |-  ( ph -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) -> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
93 92 eximdv 
 |-  ( ph -> ( E. h h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) -> E. h h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
94 13 93 mpi 
 |-  ( ph -> E. h h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) )
95 fz1iso 
 |-  ( ( < Or H /\ H e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
96 2 1 95 syl2anc 
 |-  ( ph -> E. g g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
97 exdistrv 
 |-  ( E. h E. g ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) <-> ( E. h h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ E. g g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) )
98 94 96 97 sylanbrc 
 |-  ( ph -> E. h E. g ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) )
99 isocnv 
 |-  ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) -> `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) )
100 99 ad2antrl 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) )
101 simprr 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
102 isotr 
 |-  ( ( `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
103 100 101 102 syl2anc 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
104 103 ex 
 |-  ( ph -> ( ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) ) )
105 104 2eximdv 
 |-  ( ph -> ( E. h E. g ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) -> E. h E. g ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) ) )
106 98 105 mpd 
 |-  ( ph -> E. h E. g ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
107 vex 
 |-  g e. _V
108 vex 
 |-  h e. _V
109 108 cnvex 
 |-  `' h e. _V
110 107 109 coex 
 |-  ( g o. `' h ) e. _V
111 isoeq1 
 |-  ( f = ( g o. `' h ) -> ( f Isom < , < ( ( M ... N ) , H ) <-> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) ) )
112 110 111 spcev 
 |-  ( ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) )
113 112 a1i 
 |-  ( ph -> ( ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) ) )
114 113 exlimdvv 
 |-  ( ph -> ( E. h E. g ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) ) )
115 106 114 mpd 
 |-  ( ph -> E. f f Isom < , < ( ( M ... N ) , H ) )
116 ltwefz 
 |-  < We ( M ... N )
117 wemoiso 
 |-  ( < We ( M ... N ) -> E* f f Isom < , < ( ( M ... N ) , H ) )
118 116 117 mp1i 
 |-  ( ph -> E* f f Isom < , < ( ( M ... N ) , H ) )
119 df-eu 
 |-  ( E! f f Isom < , < ( ( M ... N ) , H ) <-> ( E. f f Isom < , < ( ( M ... N ) , H ) /\ E* f f Isom < , < ( ( M ... N ) , H ) ) )
120 115 118 119 sylanbrc 
 |-  ( ph -> E! f f Isom < , < ( ( M ... N ) , H ) )