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 syl5eq ⊢ ( 𝐻 = ∅ → 𝑁 = ( 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 syl5eq ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) = ( ( ♯ ‘ 𝐻 ) + ( ( 𝑀 − 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 < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )