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 φ H Fin
fzisoeu.or φ < Or H
fzisoeu.m φ M
fzisoeu.4 N = H + M - 1
Assertion fzisoeu φ ∃! f f Isom < , < M N H

Proof

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