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 addlidd ⊢ ( 𝜑 → ( 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 bilani ⊢ ( ( 𝜑 ∧ 𝐻 = ∅ ) → ∅ = 𝐻 )
37 20 34 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐻 = ∅ ) → ( 𝑀 ... 𝑁 ) = 𝐻 )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝐻 = ∅ ) → ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) = ( ♯ ‘ 𝐻 ) )
39 22 21 pncan3d ⊢ ( 𝜑 → ( 1 + ( 𝑀 − 1 ) ) = 𝑀 )
40 39 eqcomd ⊢ ( 𝜑 → 𝑀 = ( 1 + ( 𝑀 − 1 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝑀 = ( 1 + ( 𝑀 − 1 ) ) )
42 1red ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 1 ∈ ℝ )
43 neqne ⊢ ( ¬ 𝐻 = ∅ → 𝐻 ≠ ∅ )
44 43 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝐻 ≠ ∅ )
45 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝐻 ∈ Fin )
46 hashnncl ⊢ ( 𝐻 ∈ Fin → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
48 44 47 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ♯ ‘ 𝐻 ) ∈ ℕ )
49 48 nnred ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ♯ ‘ 𝐻 ) ∈ ℝ )
50 29 zred ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( 𝑀 − 1 ) ∈ ℝ )
52 48 nnge1d ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 1 ≤ ( ♯ ‘ 𝐻 ) )
53 42 49 51 52 leadd1dd ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( 1 + ( 𝑀 − 1 ) ) ≤ ( ( ♯ ‘ 𝐻 ) + ( 𝑀 − 1 ) ) )
54 53 4 breqtrrdi ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( 1 + ( 𝑀 − 1 ) ) ≤ 𝑁 )
55 41 54 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝑀 ≤ 𝑁 )
56 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝑀 ∈ ℤ )
57 hashcl ⊢ ( 𝐻 ∈ Fin → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
58 nn0z ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ0 → ( ♯ ‘ 𝐻 ) ∈ ℤ )
59 1 57 58 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℤ )
60 59 29 zaddcld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) + ( 𝑀 − 1 ) ) ∈ ℤ )
61 4 60 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
62 61 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝑁 ∈ ℤ )
63 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
64 56 62 63 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
65 55 64 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
66 hashfz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑁 − 𝑀 ) + 1 ) )
67 65 66 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) = ( ( 𝑁 − 𝑀 ) + 1 ) )
68 4 oveq1i ⊢ ( 𝑁 − 𝑀 ) = ( ( ( ♯ ‘ 𝐻 ) + ( 𝑀 − 1 ) ) − 𝑀 )
69 1 57 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
70 69 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℂ )
71 70 23 21 addsubassd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) + ( 𝑀 − 1 ) ) − 𝑀 ) = ( ( ♯ ‘ 𝐻 ) + ( ( 𝑀 − 1 ) − 𝑀 ) ) )
72 68 71 eqtrid ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) = ( ( ♯ ‘ 𝐻 ) + ( ( 𝑀 − 1 ) − 𝑀 ) ) )
73 22 negcld ⊢ ( 𝜑 → - 1 ∈ ℂ )
74 21 22 negsubd ⊢ ( 𝜑 → ( 𝑀 + - 1 ) = ( 𝑀 − 1 ) )
75 74 eqcomd ⊢ ( 𝜑 → ( 𝑀 − 1 ) = ( 𝑀 + - 1 ) )
76 21 73 75 mvrladdd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) − 𝑀 ) = - 1 )
77 76 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) + ( ( 𝑀 − 1 ) − 𝑀 ) ) = ( ( ♯ ‘ 𝐻 ) + - 1 ) )
78 72 77 eqtrd ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) = ( ( ♯ ‘ 𝐻 ) + - 1 ) )
79 78 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 1 ) = ( ( ( ♯ ‘ 𝐻 ) + - 1 ) + 1 ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ( 𝑁 − 𝑀 ) + 1 ) = ( ( ( ♯ ‘ 𝐻 ) + - 1 ) + 1 ) )
81 70 22 negsubd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) + - 1 ) = ( ( ♯ ‘ 𝐻 ) − 1 ) )
82 81 oveq1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) + - 1 ) + 1 ) = ( ( ( ♯ ‘ 𝐻 ) − 1 ) + 1 ) )
83 70 22 npcand ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
84 82 83 eqtrd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) + - 1 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ( ( ♯ ‘ 𝐻 ) + - 1 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
86 67 80 85 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐻 = ∅ ) → ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) = ( ♯ ‘ 𝐻 ) )
87 38 86 pm2.61dan ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) = ( ♯ ‘ 𝐻 ) )
88 87 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) = ( 1 ... ( ♯ ‘ 𝐻 ) ) )
89 isoeq4 ⊢ ( ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) = ( 1 ... ( ♯ ‘ 𝐻 ) ) → ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) , ( 𝑀 ... 𝑁 ) ) ↔ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ) )
90 88 89 syl ⊢ ( 𝜑 → ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) , ( 𝑀 ... 𝑁 ) ) ↔ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ) )
91 90 biimpd ⊢ ( 𝜑 → ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) , ( 𝑀 ... 𝑁 ) ) → ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ) )
92 91 eximdv ⊢ ( 𝜑 → ( ∃ ℎ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝑀 ... 𝑁 ) ) ) , ( 𝑀 ... 𝑁 ) ) → ∃ ℎ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ) )
93 13 92 mpi ⊢ ( 𝜑 → ∃ ℎ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) )
94 fz1iso ⊢ ( ( < Or 𝐻 ∧ 𝐻 ∈ Fin ) → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) )
95 2 1 94 syl2anc ⊢ ( 𝜑 → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) )
96 exdistrv ⊢ ( ∃ ℎ ∃ 𝑔 ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) ↔ ( ∃ ℎ ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) )
97 93 95 96 sylanbrc ⊢ ( 𝜑 → ∃ ℎ ∃ 𝑔 ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) )
98 isocnv ⊢ ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) → ◡ ℎ Isom < , < ( ( 𝑀 ... 𝑁 ) , ( 1 ... ( ♯ ‘ 𝐻 ) ) ) )
99 98 ad2antrl ⊢ ( ( 𝜑 ∧ ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) ) → ◡ ℎ Isom < , < ( ( 𝑀 ... 𝑁 ) , ( 1 ... ( ♯ ‘ 𝐻 ) ) ) )
100 simprr ⊢ ( ( 𝜑 ∧ ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) ) → 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) )
101 isotr ⊢ ( ( ◡ ℎ Isom < , < ( ( 𝑀 ... 𝑁 ) , ( 1 ... ( ♯ ‘ 𝐻 ) ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) → ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
102 99 100 101 syl2anc ⊢ ( ( 𝜑 ∧ ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) ) → ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
103 102 ex ⊢ ( 𝜑 → ( ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) → ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
104 103 2eximdv ⊢ ( 𝜑 → ( ∃ ℎ ∃ 𝑔 ( ℎ Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , ( 𝑀 ... 𝑁 ) ) ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐻 ) ) , 𝐻 ) ) → ∃ ℎ ∃ 𝑔 ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
105 97 104 mpd ⊢ ( 𝜑 → ∃ ℎ ∃ 𝑔 ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
106 vex ⊢ 𝑔 ∈ V
107 vex ⊢ ℎ ∈ V
108 107 cnvex ⊢ ◡ ℎ ∈ V
109 106 108 coex ⊢ ( 𝑔 ∘ ◡ ℎ ) ∈ V
110 isoeq1 ⊢ ( 𝑓 = ( 𝑔 ∘ ◡ ℎ ) → ( 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ↔ ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
111 109 110 spcev ⊢ ( ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) → ∃ 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
112 111 a1i ⊢ ( 𝜑 → ( ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) → ∃ 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
113 112 exlimdvv ⊢ ( 𝜑 → ( ∃ ℎ ∃ 𝑔 ( 𝑔 ∘ ◡ ℎ ) Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) → ∃ 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
114 105 113 mpd ⊢ ( 𝜑 → ∃ 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
115 ltwefz ⊢ < We ( 𝑀 ... 𝑁 )
116 wemoiso ⊢ ( < We ( 𝑀 ... 𝑁 ) → ∃* 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
117 115 116 mp1i ⊢ ( 𝜑 → ∃* 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )
118 df-eu ⊢ ( ∃! 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ↔ ( ∃ 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ∧ ∃* 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) ) )
119 114 117 118 sylanbrc ⊢ ( 𝜑 → ∃! 𝑓 𝑓 Isom < , < ( ( 𝑀 ... 𝑁 ) , 𝐻 ) )