Step |
Hyp |
Ref |
Expression |
1 |
|
poimir.0 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
2 |
|
poimir.i |
⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) |
3 |
|
poimir.r |
⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) |
4 |
|
poimir.1 |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) ) |
5 |
|
poimir.2 |
⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 0 ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) |
6 |
|
poimir.3 |
⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 1 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
7 |
1 2 3 4 5 6
|
poimirlem32 |
⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
8 |
|
ovex |
⊢ ( 1 ... 𝑁 ) ∈ V |
9 |
|
retopon |
⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) |
10 |
3
|
pttoponconst |
⊢ ( ( ( 1 ... 𝑁 ) ∈ V ∧ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ) → 𝑅 ∈ ( TopOn ‘ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ) |
11 |
8 9 10
|
mp2an |
⊢ 𝑅 ∈ ( TopOn ‘ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
12 |
11
|
topontopi |
⊢ 𝑅 ∈ Top |
13 |
|
reex |
⊢ ℝ ∈ V |
14 |
|
unitssre |
⊢ ( 0 [,] 1 ) ⊆ ℝ |
15 |
|
mapss |
⊢ ( ( ℝ ∈ V ∧ ( 0 [,] 1 ) ⊆ ℝ ) → ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
16 |
13 14 15
|
mp2an |
⊢ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) |
17 |
2 16
|
eqsstri |
⊢ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) |
18 |
11
|
toponunii |
⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = ∪ 𝑅 |
19 |
18
|
restuni |
⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝐼 = ∪ ( 𝑅 ↾t 𝐼 ) ) |
20 |
12 17 19
|
mp2an |
⊢ 𝐼 = ∪ ( 𝑅 ↾t 𝐼 ) |
21 |
20 18
|
cnf |
⊢ ( 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) → 𝐹 : 𝐼 ⟶ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
22 |
4 21
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
23 |
22
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
24 |
|
elmapi |
⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ ℝ ) |
25 |
23 24
|
syl |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ ℝ ) |
26 |
25
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ) |
27 |
|
recn |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℂ ) |
28 |
|
absrpcl |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) |
29 |
28
|
ex |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℂ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) ) |
30 |
27 29
|
syl |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) ) |
31 |
|
ltsubrp |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) |
32 |
|
ltaddrp |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) |
33 |
31 32
|
jca |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
34 |
33
|
ex |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ+ → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
35 |
30 34
|
syld |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
36 |
27
|
abscld |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ ) |
37 |
|
resubcl |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ ) |
38 |
36 37
|
mpdan |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ ) |
39 |
38
|
rexrd |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ* ) |
40 |
|
readdcl |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ ) |
41 |
36 40
|
mpdan |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ ) |
42 |
41
|
rexrd |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ* ) |
43 |
|
rexr |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ* ) |
44 |
|
elioo5 |
⊢ ( ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ* ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ∈ ℝ* ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
45 |
39 42 43 44
|
syl3anc |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
46 |
35 45
|
sylibrd |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
47 |
26 46
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
48 |
|
fveq2 |
⊢ ( 𝑥 = 𝑐 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑐 ) ) |
49 |
48
|
fveq1d |
⊢ ( 𝑥 = 𝑐 → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) |
50 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) |
51 |
|
fvex |
⊢ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ V |
52 |
49 50 51
|
fvmpt |
⊢ ( 𝑐 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) = ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) |
53 |
52
|
eleq1d |
⊢ ( 𝑐 ∈ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
54 |
53
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
55 |
47 54
|
sylibrd |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
56 |
|
iooretop |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∈ ( topGen ‘ ran (,) ) |
57 |
|
resttopon |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( 𝑅 ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) ) |
58 |
11 17 57
|
mp2an |
⊢ ( 𝑅 ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) |
59 |
58
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑅 ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) ) |
60 |
22
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
61 |
60 4
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) ) |
62 |
61
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) ) |
63 |
11
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ ( TopOn ‘ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ) |
64 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
65 |
64
|
fconst6 |
⊢ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top |
66 |
18 3
|
ptpjcn |
⊢ ( ( ( 1 ... 𝑁 ) ∈ V ∧ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝑧 ‘ 𝑛 ) ) ∈ ( 𝑅 Cn ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ) ) |
67 |
8 65 66
|
mp3an12 |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑧 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝑧 ‘ 𝑛 ) ) ∈ ( 𝑅 Cn ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ) ) |
68 |
|
fvex |
⊢ ( topGen ‘ ran (,) ) ∈ V |
69 |
68
|
fvconst2 |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) = ( topGen ‘ ran (,) ) ) |
70 |
69
|
oveq2d |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑅 Cn ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ) = ( 𝑅 Cn ( topGen ‘ ran (,) ) ) ) |
71 |
67 70
|
eleqtrd |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑧 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝑧 ‘ 𝑛 ) ) ∈ ( 𝑅 Cn ( topGen ‘ ran (,) ) ) ) |
72 |
71
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝑧 ‘ 𝑛 ) ) ∈ ( 𝑅 Cn ( topGen ‘ ran (,) ) ) ) |
73 |
|
fveq1 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑧 ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) |
74 |
59 62 63 72 73
|
cnmpt11 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( 𝑅 ↾t 𝐼 ) Cn ( topGen ‘ ran (,) ) ) ) |
75 |
20
|
cncnpi |
⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( 𝑅 ↾t 𝐼 ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑐 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ) |
76 |
74 75
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑐 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ) |
77 |
76
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ) |
78 |
|
iscnp |
⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) ∧ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ 𝑐 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) : 𝐼 ⟶ ℝ ∧ ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ) ) ) |
79 |
58 9 78
|
mp3an12 |
⊢ ( 𝑐 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) : 𝐼 ⟶ ℝ ∧ ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ) ) ) |
80 |
79
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∈ ( ( ( 𝑅 ↾t 𝐼 ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑐 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) : 𝐼 ⟶ ℝ ∧ ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ) ) ) |
81 |
77 80
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) : 𝐼 ⟶ ℝ ∧ ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ) ) |
82 |
81
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ) |
83 |
|
eleq2 |
⊢ ( 𝑧 = ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
84 |
|
sseq2 |
⊢ ( 𝑧 = ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
85 |
84
|
anbi2d |
⊢ ( 𝑧 = ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ↔ ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) |
86 |
85
|
rexbidv |
⊢ ( 𝑧 = ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ↔ ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) |
87 |
83 86
|
imbi12d |
⊢ ( 𝑧 = ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) ↔ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) ) |
88 |
87
|
rspcv |
⊢ ( ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∈ ( topGen ‘ ran (,) ) → ( ∀ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ 𝑧 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ 𝑧 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) ) |
89 |
56 82 88
|
mpsyl |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑐 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) |
90 |
55 89
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) ) |
91 |
|
0re |
⊢ 0 ∈ ℝ |
92 |
|
letric |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) |
93 |
26 91 92
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) |
94 |
90 93
|
jctird |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
95 |
|
r19.41v |
⊢ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) |
96 |
|
anass |
⊢ ( ( ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
97 |
96
|
rexbii |
⊢ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
98 |
95 97
|
bitr3i |
⊢ ( ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
99 |
94 98
|
syl6ib |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
100 |
58
|
topontopi |
⊢ ( 𝑅 ↾t 𝐼 ) ∈ Top |
101 |
20
|
eltopss |
⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ Top ∧ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ) → 𝑣 ⊆ 𝐼 ) |
102 |
100 101
|
mpan |
⊢ ( 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) → 𝑣 ⊆ 𝐼 ) |
103 |
|
fvex |
⊢ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ∈ V |
104 |
103 50
|
dmmpti |
⊢ dom ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) = 𝐼 |
105 |
104
|
sseq2i |
⊢ ( 𝑣 ⊆ dom ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ↔ 𝑣 ⊆ 𝐼 ) |
106 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) |
107 |
|
funimass4 |
⊢ ( ( Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ∧ 𝑣 ⊆ dom ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
108 |
106 107
|
mpan |
⊢ ( 𝑣 ⊆ dom ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
109 |
105 108
|
sylbir |
⊢ ( 𝑣 ⊆ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
110 |
|
ssel2 |
⊢ ( ( 𝑣 ⊆ 𝐼 ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ 𝐼 ) |
111 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) |
112 |
111
|
fveq1d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
113 |
|
fvex |
⊢ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∈ V |
114 |
112 50 113
|
fvmpt |
⊢ ( 𝑧 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
115 |
114
|
eleq1d |
⊢ ( 𝑧 ∈ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
116 |
|
eliooord |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) |
117 |
115 116
|
syl6bi |
⊢ ( 𝑧 ∈ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
118 |
110 117
|
syl |
⊢ ( ( 𝑣 ⊆ 𝐼 ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
119 |
118
|
ralimdva |
⊢ ( 𝑣 ⊆ 𝐼 → ( ∀ 𝑧 ∈ 𝑣 ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
120 |
109 119
|
sylbid |
⊢ ( 𝑣 ⊆ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
121 |
120
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) ) |
122 |
|
absnid |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = - ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) |
123 |
122
|
oveq2d |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + - ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) |
124 |
27
|
negidd |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + - ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = 0 ) |
125 |
124
|
adantr |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + - ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = 0 ) |
126 |
123 125
|
eqtrd |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
127 |
26 126
|
sylan |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
128 |
127
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
129 |
128
|
breq2d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < 0 ) ) |
130 |
22
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) |
131 |
|
elmapi |
⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) : ( 1 ... 𝑁 ) ⟶ ℝ ) |
132 |
130 131
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) : ( 1 ... 𝑁 ) ⟶ ℝ ) |
133 |
132
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∈ ℝ ) |
134 |
133
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∈ ℝ ) |
135 |
|
0red |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → 0 ∈ ℝ ) |
136 |
134 135
|
ltnled |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
137 |
136
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
138 |
137
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
139 |
129 138
|
bitrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
140 |
139
|
biimpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
141 |
110 140
|
sylan2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ ( 𝑣 ⊆ 𝐼 ∧ 𝑧 ∈ 𝑣 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
142 |
141
|
anassrs |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑣 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
143 |
142
|
adantld |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑣 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
144 |
143
|
ralimdva |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) ∧ 𝑣 ⊆ 𝐼 ) → ( ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
145 |
144
|
an32s |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ) → ( ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
146 |
145
|
impancom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 → ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
147 |
|
absid |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) |
148 |
147
|
oveq2d |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) |
149 |
27
|
subidd |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = 0 ) |
150 |
149
|
adantr |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) = 0 ) |
151 |
148 150
|
eqtrd |
⊢ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
152 |
26 151
|
sylan |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
153 |
152
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) = 0 ) |
154 |
153
|
breq1d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ 0 < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
155 |
135 134
|
ltnled |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 0 < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
156 |
155
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 0 < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
157 |
156
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 0 < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
158 |
154 157
|
bitrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
159 |
158
|
biimpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) → ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
160 |
110 159
|
sylan2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ ( 𝑣 ⊆ 𝐼 ∧ 𝑧 ∈ 𝑣 ) ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) → ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
161 |
160
|
anassrs |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) → ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
162 |
161
|
adantrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
163 |
162
|
ralimdva |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ∧ 𝑣 ⊆ 𝐼 ) → ( ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
164 |
163
|
an32s |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
165 |
164
|
impancom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) → ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
166 |
146 165
|
orim12d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) ∧ ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ) → ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) |
167 |
166
|
expimpd |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) → ( ( ∀ 𝑧 ∈ 𝑣 ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) < ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) < ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) |
168 |
121 167
|
syland |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ⊆ 𝐼 ) → ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) |
169 |
102 168
|
sylan2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ) → ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) |
170 |
169
|
anim2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ) → ( ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) ) |
171 |
170
|
reximdva |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) “ 𝑣 ) ⊆ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) (,) ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) + ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≤ 0 ∨ 0 ≤ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) ) |
172 |
99 171
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) ) |
173 |
|
ralnex |
⊢ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
174 |
173
|
rexbii |
⊢ ( ∃ 𝑟 ∈ { ≤ , ◡ ≤ } ∀ 𝑧 ∈ 𝑣 ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ∃ 𝑟 ∈ { ≤ , ◡ ≤ } ¬ ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
175 |
|
letsr |
⊢ ≤ ∈ TosetRel |
176 |
175
|
elexi |
⊢ ≤ ∈ V |
177 |
176
|
cnvex |
⊢ ◡ ≤ ∈ V |
178 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
179 |
178
|
notbid |
⊢ ( 𝑟 = ≤ → ( ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
180 |
179
|
ralbidv |
⊢ ( 𝑟 = ≤ → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
181 |
|
breq |
⊢ ( 𝑟 = ◡ ≤ → ( 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ 0 ◡ ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
182 |
|
c0ex |
⊢ 0 ∈ V |
183 |
182 113
|
brcnv |
⊢ ( 0 ◡ ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) |
184 |
181 183
|
syl6bb |
⊢ ( 𝑟 = ◡ ≤ → ( 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
185 |
184
|
notbid |
⊢ ( 𝑟 = ◡ ≤ → ( ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
186 |
185
|
ralbidv |
⊢ ( 𝑟 = ◡ ≤ → ( ∀ 𝑧 ∈ 𝑣 ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
187 |
176 177 180 186
|
rexpr |
⊢ ( ∃ 𝑟 ∈ { ≤ , ◡ ≤ } ∀ 𝑧 ∈ 𝑣 ¬ 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) |
188 |
|
rexnal |
⊢ ( ∃ 𝑟 ∈ { ≤ , ◡ ≤ } ¬ ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ ¬ ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
189 |
174 187 188
|
3bitr3i |
⊢ ( ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ↔ ¬ ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) |
190 |
189
|
anbi2i |
⊢ ( ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ↔ ( 𝑐 ∈ 𝑣 ∧ ¬ ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
191 |
|
annim |
⊢ ( ( 𝑐 ∈ 𝑣 ∧ ¬ ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ↔ ¬ ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
192 |
190 191
|
bitri |
⊢ ( ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ↔ ¬ ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
193 |
192
|
rexbii |
⊢ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ↔ ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ¬ ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
194 |
|
rexnal |
⊢ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ¬ ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ↔ ¬ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
195 |
193 194
|
bitri |
⊢ ( ∃ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 ∧ ( ∀ 𝑧 ∈ 𝑣 ¬ 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ∨ ∀ 𝑧 ∈ 𝑣 ¬ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ↔ ¬ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) |
196 |
172 195
|
syl6ib |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) ≠ 0 → ¬ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) ) |
197 |
196
|
necon4ad |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) = 0 ) ) |
198 |
197
|
ralimdva |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) = 0 ) ) |
199 |
25
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑐 ) Fn ( 1 ... 𝑁 ) ) |
200 |
198 199
|
jctild |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑐 ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) = 0 ) ) ) |
201 |
|
fconstfv |
⊢ ( ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ { 0 } ↔ ( ( 𝐹 ‘ 𝑐 ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) = 0 ) ) |
202 |
182
|
fconst2 |
⊢ ( ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ { 0 } ↔ ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) |
203 |
201 202
|
bitr3i |
⊢ ( ( ( 𝐹 ‘ 𝑐 ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) = 0 ) ↔ ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) |
204 |
200 203
|
syl6ib |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) ) |
205 |
204
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ∃ 𝑐 ∈ 𝐼 ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) ) |
206 |
7 205
|
mpd |
⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) |