Step | Hyp | Ref
| Expression |
1 | | fzssz 12343 |
. . . . . . . . 9
⊢ (𝑀...𝑁) ⊆ ℤ |
2 | | zssre 11384 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
3 | 1, 2 | sstri 3612 |
. . . . . . . 8
⊢ (𝑀...𝑁) ⊆ ℝ |
4 | | ltso 10118 |
. . . . . . . 8
⊢ < Or
ℝ |
5 | | soss 5053 |
. . . . . . . 8
⊢ ((𝑀...𝑁) ⊆ ℝ → ( < Or ℝ
→ < Or (𝑀...𝑁))) |
6 | 3, 4, 5 | mp2 9 |
. . . . . . 7
⊢ < Or
(𝑀...𝑁) |
7 | | fzfi 12771 |
. . . . . . 7
⊢ (𝑀...𝑁) ∈ Fin |
8 | | fz1iso 13246 |
. . . . . . 7
⊢ (( <
Or (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → ∃ℎ ℎ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁))) |
9 | 6, 7, 8 | mp2an 708 |
. . . . . 6
⊢
∃ℎ ℎ Isom < , <
((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) |
10 | | fzisoeu.4 |
. . . . . . . . . . . . . . . 16
⊢ 𝑁 = ((#‘𝐻) + (𝑀 − 1)) |
11 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐻 = ∅ → (#‘𝐻) =
(#‘∅)) |
12 | | hash0 13158 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘∅) = 0 |
13 | 11, 12 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 = ∅ → (#‘𝐻) = 0) |
14 | 13 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 = ∅ →
((#‘𝐻) + (𝑀 − 1)) = (0 + (𝑀 − 1))) |
15 | 10, 14 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 = ∅ → 𝑁 = (0 + (𝑀 − 1))) |
16 | 15 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝐻 = ∅ → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1)))) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1)))) |
18 | | fzisoeu.m |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | 18 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℂ) |
20 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℂ) |
21 | 19, 20 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) ∈ ℂ) |
22 | 21 | addid2d 10237 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 + (𝑀 − 1)) = (𝑀 − 1)) |
23 | 22 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = (𝑀...(𝑀 − 1))) |
24 | 18 | zred 11482 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℝ) |
25 | 24 | ltm1d 10956 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
26 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
27 | 18, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
28 | | fzn 12357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
29 | 18, 27, 28 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
30 | 25, 29 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
31 | 23, 30 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = ∅) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...(0 + (𝑀 − 1))) = ∅) |
33 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 = ∅ ↔ ∅ =
𝐻) |
34 | 33 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (𝐻 = ∅ → ∅ =
𝐻) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 = ∅) → ∅ = 𝐻) |
36 | 17, 32, 35 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = 𝐻) |
37 | 36 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐻 = ∅) → (#‘(𝑀...𝑁)) = (#‘𝐻)) |
38 | 20, 19 | pncan3d 10395 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀) |
39 | 38 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 = (1 + (𝑀 − 1))) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 = (1 + (𝑀 − 1))) |
41 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ∈
ℝ) |
42 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝐻 = ∅ → 𝐻 ≠ ∅) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ≠ ∅) |
44 | | fzisoeu.h |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻 ∈ Fin) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ∈ Fin) |
46 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻 ∈ Fin →
((#‘𝐻) ∈ ℕ
↔ 𝐻 ≠
∅)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) |
48 | 43, 47 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘𝐻) ∈
ℕ) |
49 | 48 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘𝐻) ∈
ℝ) |
50 | 27 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑀 − 1) ∈ ℝ) |
52 | 48 | nnge1d 11063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ≤ (#‘𝐻)) |
53 | 41, 49, 51, 52 | leadd1dd 10641 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ ((#‘𝐻) + (𝑀 − 1))) |
54 | 53, 10 | syl6breqr 4695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ 𝑁) |
55 | 40, 54 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ≤ 𝑁) |
56 | 18 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ∈ ℤ) |
57 | | hashcl 13147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ∈ Fin →
(#‘𝐻) ∈
ℕ0) |
58 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐻) ∈
ℕ0 → (#‘𝐻) ∈ ℤ) |
59 | 44, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (#‘𝐻) ∈ ℤ) |
60 | 59, 27 | zaddcld 11486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((#‘𝐻) + (𝑀 − 1)) ∈
ℤ) |
61 | 10, 60 | syl5eqel 2705 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ ℤ) |
63 | | eluz 11701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
64 | 56, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
65 | 55, 64 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ (ℤ≥‘𝑀)) |
66 | | hashfz 13214 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (#‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1)) |
68 | 10 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 − 𝑀) = (((#‘𝐻) + (𝑀 − 1)) − 𝑀) |
69 | 44, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (#‘𝐻) ∈
ℕ0) |
70 | 69 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (#‘𝐻) ∈ ℂ) |
71 | 70, 21, 19 | addsubassd 10412 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((#‘𝐻) + (𝑀 − 1)) − 𝑀) = ((#‘𝐻) + ((𝑀 − 1) − 𝑀))) |
72 | 68, 71 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 𝑀) = ((#‘𝐻) + ((𝑀 − 1) − 𝑀))) |
73 | 19, 20 | negsubd 10398 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + -1) = (𝑀 − 1)) |
74 | 73 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 − 1) = (𝑀 + -1)) |
75 | 74 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 − 1) − 𝑀) = ((𝑀 + -1) − 𝑀)) |
76 | 20 | negcld 10379 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -1 ∈
ℂ) |
77 | 19, 76 | pncan2d 10394 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + -1) − 𝑀) = -1) |
78 | 75, 77 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 − 1) − 𝑀) = -1) |
79 | 78 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐻) + ((𝑀 − 1) − 𝑀)) = ((#‘𝐻) + -1)) |
80 | 72, 79 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 𝑀) = ((#‘𝐻) + -1)) |
81 | 80 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (((#‘𝐻) + -1) + 1)) |
82 | 81 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((𝑁 − 𝑀) + 1) = (((#‘𝐻) + -1) + 1)) |
83 | 70, 20 | negsubd 10398 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐻) + -1) = ((#‘𝐻) − 1)) |
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((#‘𝐻) + -1) + 1) = (((#‘𝐻) − 1) +
1)) |
85 | 70, 20 | npcand 10396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((#‘𝐻) − 1) + 1) =
(#‘𝐻)) |
86 | 84, 85 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((#‘𝐻) + -1) + 1) = (#‘𝐻)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (((#‘𝐻) + -1) + 1) = (#‘𝐻)) |
88 | 67, 82, 87 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘(𝑀...𝑁)) = (#‘𝐻)) |
89 | 37, 88 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝑀...𝑁)) = (#‘𝐻)) |
90 | 89 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (1...(#‘(𝑀...𝑁))) = (1...(#‘𝐻))) |
91 | | isoeq4 6570 |
. . . . . . . . 9
⊢
((1...(#‘(𝑀...𝑁))) = (1...(#‘𝐻)) → (ℎ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)))) |
92 | 90, 91 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℎ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)))) |
93 | 92 | biimpd 219 |
. . . . . . 7
⊢ (𝜑 → (ℎ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) → ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)))) |
94 | 93 | eximdv 1846 |
. . . . . 6
⊢ (𝜑 → (∃ℎ ℎ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) → ∃ℎ ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)))) |
95 | 9, 94 | mpi 20 |
. . . . 5
⊢ (𝜑 → ∃ℎ ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁))) |
96 | | fzisoeu.or |
. . . . . 6
⊢ (𝜑 → < Or 𝐻) |
97 | | fz1iso 13246 |
. . . . . 6
⊢ (( <
Or 𝐻 ∧ 𝐻 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) |
98 | 96, 44, 97 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) |
99 | | eeanv 2182 |
. . . . 5
⊢
(∃ℎ∃𝑔(ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) ↔ (∃ℎ ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) |
100 | 95, 98, 99 | sylanbrc 698 |
. . . 4
⊢ (𝜑 → ∃ℎ∃𝑔(ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) |
101 | | isocnv 6580 |
. . . . . . . 8
⊢ (ℎ Isom < , <
((1...(#‘𝐻)), (𝑀...𝑁)) → ◡ℎ Isom < , < ((𝑀...𝑁), (1...(#‘𝐻)))) |
102 | 101 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → ◡ℎ Isom < , < ((𝑀...𝑁), (1...(#‘𝐻)))) |
103 | | simprr 796 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) |
104 | | isotr 6586 |
. . . . . . 7
⊢ ((◡ℎ Isom < , < ((𝑀...𝑁), (1...(#‘𝐻))) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → (𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)) |
105 | 102, 103,
104 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → (𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)) |
106 | 105 | ex 450 |
. . . . 5
⊢ (𝜑 → ((ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → (𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))) |
107 | 106 | 2eximdv 1848 |
. . . 4
⊢ (𝜑 → (∃ℎ∃𝑔(ℎ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → ∃ℎ∃𝑔(𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))) |
108 | 100, 107 | mpd 15 |
. . 3
⊢ (𝜑 → ∃ℎ∃𝑔(𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)) |
109 | | vex 3203 |
. . . . . . 7
⊢ 𝑔 ∈ V |
110 | | vex 3203 |
. . . . . . . 8
⊢ ℎ ∈ V |
111 | 110 | cnvex 7113 |
. . . . . . 7
⊢ ◡ℎ ∈ V |
112 | 109, 111 | coex 7118 |
. . . . . 6
⊢ (𝑔 ∘ ◡ℎ) ∈ V |
113 | | isoeq1 6567 |
. . . . . 6
⊢ (𝑓 = (𝑔 ∘ ◡ℎ) → (𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))) |
114 | 112, 113 | spcev 3300 |
. . . . 5
⊢ ((𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) |
115 | 114 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))) |
116 | 115 | exlimdvv 1862 |
. . 3
⊢ (𝜑 → (∃ℎ∃𝑔(𝑔 ∘ ◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))) |
117 | 108, 116 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) |
118 | | ltwefz 12762 |
. . 3
⊢ < We
(𝑀...𝑁) |
119 | | wemoiso 7153 |
. . 3
⊢ ( < We
(𝑀...𝑁) → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) |
120 | 118, 119 | mp1i 13 |
. 2
⊢ (𝜑 → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) |
121 | | eu5 2496 |
. 2
⊢
(∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ∧ ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))) |
122 | 117, 120,
121 | sylanbrc 698 |
1
⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) |