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 addlidd 
 |-  ( 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 bilani 
 |-  ( ( ph /\ H = (/) ) -> (/) = H )
37 20 34 36 3eqtrd 
 |-  ( ( ph /\ H = (/) ) -> ( M ... N ) = H )
38 37 fveq2d 
 |-  ( ( ph /\ H = (/) ) -> ( # ` ( M ... N ) ) = ( # ` H ) )
39 22 21 pncan3d 
 |-  ( ph -> ( 1 + ( M - 1 ) ) = M )
40 39 eqcomd 
 |-  ( ph -> M = ( 1 + ( M - 1 ) ) )
41 40 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> M = ( 1 + ( M - 1 ) ) )
42 1red 
 |-  ( ( ph /\ -. H = (/) ) -> 1 e. RR )
43 neqne 
 |-  ( -. H = (/) -> H =/= (/) )
44 43 adantl 
 |-  ( ( ph /\ -. H = (/) ) -> H =/= (/) )
45 1 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> H e. Fin )
46 hashnncl 
 |-  ( H e. Fin -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
47 45 46 syl 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
48 44 47 mpbird 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` H ) e. NN )
49 48 nnred 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` H ) e. RR )
50 29 zred 
 |-  ( ph -> ( M - 1 ) e. RR )
51 50 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( M - 1 ) e. RR )
52 48 nnge1d 
 |-  ( ( ph /\ -. H = (/) ) -> 1 <_ ( # ` H ) )
53 42 49 51 52 leadd1dd 
 |-  ( ( ph /\ -. H = (/) ) -> ( 1 + ( M - 1 ) ) <_ ( ( # ` H ) + ( M - 1 ) ) )
54 53 4 breqtrrdi 
 |-  ( ( ph /\ -. H = (/) ) -> ( 1 + ( M - 1 ) ) <_ N )
55 41 54 eqbrtrd 
 |-  ( ( ph /\ -. H = (/) ) -> M <_ N )
56 3 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> M e. ZZ )
57 hashcl 
 |-  ( H e. Fin -> ( # ` H ) e. NN0 )
58 nn0z 
 |-  ( ( # ` H ) e. NN0 -> ( # ` H ) e. ZZ )
59 1 57 58 3syl 
 |-  ( ph -> ( # ` H ) e. ZZ )
60 59 29 zaddcld 
 |-  ( ph -> ( ( # ` H ) + ( M - 1 ) ) e. ZZ )
61 4 60 eqeltrid 
 |-  ( ph -> N e. ZZ )
62 61 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> N e. ZZ )
63 eluz 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
64 56 62 63 syl2anc 
 |-  ( ( ph /\ -. H = (/) ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
65 55 64 mpbird 
 |-  ( ( ph /\ -. H = (/) ) -> N e. ( ZZ>= ` M ) )
66 hashfz 
 |-  ( N e. ( ZZ>= ` M ) -> ( # ` ( M ... N ) ) = ( ( N - M ) + 1 ) )
67 65 66 syl 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` ( M ... N ) ) = ( ( N - M ) + 1 ) )
68 4 oveq1i 
 |-  ( N - M ) = ( ( ( # ` H ) + ( M - 1 ) ) - M )
69 1 57 syl 
 |-  ( ph -> ( # ` H ) e. NN0 )
70 69 nn0cnd 
 |-  ( ph -> ( # ` H ) e. CC )
71 70 23 21 addsubassd 
 |-  ( ph -> ( ( ( # ` H ) + ( M - 1 ) ) - M ) = ( ( # ` H ) + ( ( M - 1 ) - M ) ) )
72 68 71 eqtrid 
 |-  ( ph -> ( N - M ) = ( ( # ` H ) + ( ( M - 1 ) - M ) ) )
73 22 negcld 
 |-  ( ph -> -u 1 e. CC )
74 21 22 negsubd 
 |-  ( ph -> ( M + -u 1 ) = ( M - 1 ) )
75 74 eqcomd 
 |-  ( ph -> ( M - 1 ) = ( M + -u 1 ) )
76 21 73 75 mvrladdd 
 |-  ( ph -> ( ( M - 1 ) - M ) = -u 1 )
77 76 oveq2d 
 |-  ( ph -> ( ( # ` H ) + ( ( M - 1 ) - M ) ) = ( ( # ` H ) + -u 1 ) )
78 72 77 eqtrd 
 |-  ( ph -> ( N - M ) = ( ( # ` H ) + -u 1 ) )
79 78 oveq1d 
 |-  ( ph -> ( ( N - M ) + 1 ) = ( ( ( # ` H ) + -u 1 ) + 1 ) )
80 79 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( N - M ) + 1 ) = ( ( ( # ` H ) + -u 1 ) + 1 ) )
81 70 22 negsubd 
 |-  ( ph -> ( ( # ` H ) + -u 1 ) = ( ( # ` H ) - 1 ) )
82 81 oveq1d 
 |-  ( ph -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( ( ( # ` H ) - 1 ) + 1 ) )
83 70 22 npcand 
 |-  ( ph -> ( ( ( # ` H ) - 1 ) + 1 ) = ( # ` H ) )
84 82 83 eqtrd 
 |-  ( ph -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( # ` H ) )
85 84 adantr 
 |-  ( ( ph /\ -. H = (/) ) -> ( ( ( # ` H ) + -u 1 ) + 1 ) = ( # ` H ) )
86 67 80 85 3eqtrd 
 |-  ( ( ph /\ -. H = (/) ) -> ( # ` ( M ... N ) ) = ( # ` H ) )
87 38 86 pm2.61dan 
 |-  ( ph -> ( # ` ( M ... N ) ) = ( # ` H ) )
88 87 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` ( M ... N ) ) ) = ( 1 ... ( # ` H ) ) )
89 isoeq4 
 |-  ( ( 1 ... ( # ` ( M ... N ) ) ) = ( 1 ... ( # ` H ) ) -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) <-> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
90 88 89 syl 
 |-  ( ph -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) <-> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
91 90 biimpd 
 |-  ( ph -> ( h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) -> h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
92 91 eximdv 
 |-  ( ph -> ( E. h h Isom < , < ( ( 1 ... ( # ` ( M ... N ) ) ) , ( M ... N ) ) -> E. h h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) ) )
93 13 92 mpi 
 |-  ( ph -> E. h h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) )
94 fz1iso 
 |-  ( ( < Or H /\ H e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
95 2 1 94 syl2anc 
 |-  ( ph -> E. g g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
96 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 ) ) )
97 93 95 96 sylanbrc 
 |-  ( ph -> E. h E. g ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) )
98 isocnv 
 |-  ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) -> `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) )
99 98 ad2antrl 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) )
100 simprr 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) )
101 isotr 
 |-  ( ( `' h Isom < , < ( ( M ... N ) , ( 1 ... ( # ` H ) ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
102 99 100 101 syl2anc 
 |-  ( ( ph /\ ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
103 102 ex 
 |-  ( ph -> ( ( h Isom < , < ( ( 1 ... ( # ` H ) ) , ( M ... N ) ) /\ g Isom < , < ( ( 1 ... ( # ` H ) ) , H ) ) -> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) ) )
104 103 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 ) ) )
105 97 104 mpd 
 |-  ( ph -> E. h E. g ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) )
106 vex 
 |-  g e. _V
107 vex 
 |-  h e. _V
108 107 cnvex 
 |-  `' h e. _V
109 106 108 coex 
 |-  ( g o. `' h ) e. _V
110 isoeq1 
 |-  ( f = ( g o. `' h ) -> ( f Isom < , < ( ( M ... N ) , H ) <-> ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) ) )
111 109 110 spcev 
 |-  ( ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) )
112 111 a1i 
 |-  ( ph -> ( ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) ) )
113 112 exlimdvv 
 |-  ( ph -> ( E. h E. g ( g o. `' h ) Isom < , < ( ( M ... N ) , H ) -> E. f f Isom < , < ( ( M ... N ) , H ) ) )
114 105 113 mpd 
 |-  ( ph -> E. f f Isom < , < ( ( M ... N ) , H ) )
115 ltwefz 
 |-  < We ( M ... N )
116 wemoiso 
 |-  ( < We ( M ... N ) -> E* f f Isom < , < ( ( M ... N ) , H ) )
117 115 116 mp1i 
 |-  ( ph -> E* f f Isom < , < ( ( M ... N ) , H ) )
118 df-eu 
 |-  ( E! f f Isom < , < ( ( M ... N ) , H ) <-> ( E. f f Isom < , < ( ( M ... N ) , H ) /\ E* f f Isom < , < ( ( M ... N ) , H ) ) )
119 114 117 118 sylanbrc 
 |-  ( ph -> E! f f Isom < , < ( ( M ... N ) , H ) )