Metamath Proof Explorer

Theorem poimir

Description: Poincare-Miranda theorem. Theorem on Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimir.i ⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
poimir.r ⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
poimir.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) )
poimir.2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 0 ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 )
poimir.3 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 1 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) )
Assertion poimir ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) )

Proof

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
24 elmapi ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ ℝ )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑐 ) : ( 1 ... 𝑁 ) ⟶ ℝ )
26 25 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 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 imbitrdi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 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 biimtrdi ⊢ ( 𝑧 ∈ 𝐼 → ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑛 ) − ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
131 elmapi ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) : ( 1 ... 𝑁 ) ⟶ ℝ )
132 130 131 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) : ( 1 ... 𝑁 ) ⟶ ℝ )
133 132 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 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 bitrdi ⊢ ( 𝑟 = ◡ ≤ → ( 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 imbitrdi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑛 ∈ ( 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 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) )
205 204 reximdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) → ∃ 𝑐 ∈ 𝐼 ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) ) )
206 7 205 mpd ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ( 𝐹 ‘ 𝑐 ) = ( ( 1 ... 𝑁 ) × { 0 } ) )