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 ( 𝜑𝐻 ∈ Fin )
fzisoeu.or ( 𝜑 → < Or 𝐻 )
fzisoeu.m ( 𝜑𝑀 ∈ ℤ )
fzisoeu.4 𝑁 = ( ( ♯ ‘ 𝐻 ) + ( 𝑀 − 1 ) )
Assertion fzisoeu ( 𝜑 → ∃! 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )

Proof

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