This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem31

Description: If A is finite and for any element in A there is a number m such that a property holds for all numbers larger than m , then there is a number n such that the property holds for all numbers larger than n and for all elements in A . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 29-Sep-2020)

Ref Expression
Hypotheses fourierdlem31.i ⊢ Ⅎ 𝑖 𝜑
fourierdlem31.r ⊢ Ⅎ 𝑟 𝜑
fourierdlem31.iv ⊢ Ⅎ 𝑖 𝑉
fourierdlem31.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fourierdlem31.exm ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 )
fourierdlem31.m ⊢ 𝑀 = { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 }
fourierdlem31.v ⊢ 𝑉 = ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) )
fourierdlem31.n ⊢ 𝑁 = sup ( ran 𝑉 , ℝ , < )
Assertion fourierdlem31 ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )

Proof

Step Hyp Ref Expression
1 fourierdlem31.i ⊢ Ⅎ 𝑖 𝜑
2 fourierdlem31.r ⊢ Ⅎ 𝑟 𝜑
3 fourierdlem31.iv ⊢ Ⅎ 𝑖 𝑉
4 fourierdlem31.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 fourierdlem31.exm ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 )
6 fourierdlem31.m ⊢ 𝑀 = { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 }
7 fourierdlem31.v ⊢ 𝑉 = ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) )
8 fourierdlem31.n ⊢ 𝑁 = sup ( ran 𝑉 , ℝ , < )
9 1nn ⊢ 1 ∈ ℕ
10 rzal ⊢ ( 𝐴 = ∅ → ∀ 𝑖 ∈ 𝐴 𝜒 )
11 10 ralrimivw ⊢ ( 𝐴 = ∅ → ∀ 𝑟 ∈ ( 1 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
12 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 (,) +∞ ) = ( 1 (,) +∞ ) )
13 12 raleqdv ⊢ ( 𝑛 = 1 → ( ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ↔ ∀ 𝑟 ∈ ( 1 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ) )
14 13 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 1 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
15 9 11 14 sylancr ⊢ ( 𝐴 = ∅ → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
17 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑀 = { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } )
18 17 infeq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( 𝑀 , ℝ , < ) = inf ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } , ℝ , < ) )
19 ssrab2 ⊢ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ⊆ ℕ
20 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
21 19 20 sseqtri ⊢ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ⊆ ( ℤ≥ ‘ 1 )
22 5 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 )
23 rabn0 ⊢ ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ≠ ∅ ↔ ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 )
24 22 23 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ≠ ∅ )
25 infssuzcl ⊢ ( ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ≠ ∅ ) → inf ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } , ℝ , < ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } )
26 21 24 25 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } , ℝ , < ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } )
27 19 26 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } , ℝ , < ) ∈ ℕ )
28 18 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( 𝑀 , ℝ , < ) ∈ ℕ )
29 1 7 28 rnmptssd ⊢ ( 𝜑 → ran 𝑉 ⊆ ℕ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ran 𝑉 ⊆ ℕ )
31 ltso ⊢ < Or ℝ
32 31 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → < Or ℝ )
33 mptfi ⊢ ( 𝐴 ∈ Fin → ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) ) ∈ Fin )
34 4 33 syl ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) ) ∈ Fin )
35 7 34 eqeltrid ⊢ ( 𝜑 → 𝑉 ∈ Fin )
36 rnfi ⊢ ( 𝑉 ∈ Fin → ran 𝑉 ∈ Fin )
37 35 36 syl ⊢ ( 𝜑 → ran 𝑉 ∈ Fin )
38 37 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ran 𝑉 ∈ Fin )
39 neqne ⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
40 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ 𝐴 )
41 39 40 sylib ⊢ ( ¬ 𝐴 = ∅ → ∃ 𝑖 𝑖 ∈ 𝐴 )
42 41 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑖 𝑖 ∈ 𝐴 )
43 nfv ⊢ Ⅎ 𝑖 ¬ 𝐴 = ∅
44 1 43 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ¬ 𝐴 = ∅ )
45 3 nfrn ⊢ Ⅎ 𝑖 ran 𝑉
46 nfcv ⊢ Ⅎ 𝑖 ∅
47 45 46 nfne ⊢ Ⅎ 𝑖 ran 𝑉 ≠ ∅
48 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
49 7 elrnmpt1 ⊢ ( ( 𝑖 ∈ 𝐴 ∧ inf ( 𝑀 , ℝ , < ) ∈ ℕ ) → inf ( 𝑀 , ℝ , < ) ∈ ran 𝑉 )
50 48 28 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( 𝑀 , ℝ , < ) ∈ ran 𝑉 )
51 50 ne0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ran 𝑉 ≠ ∅ )
52 51 ex ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅ ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ( 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅ ) )
54 44 47 53 exlimd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ( ∃ 𝑖 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅ ) )
55 42 54 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ran 𝑉 ≠ ∅ )
56 nnssre ⊢ ℕ ⊆ ℝ
57 30 56 sstrdi ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ran 𝑉 ⊆ ℝ )
58 fisupcl ⊢ ( ( < Or ℝ ∧ ( ran 𝑉 ∈ Fin ∧ ran 𝑉 ≠ ∅ ∧ ran 𝑉 ⊆ ℝ ) ) → sup ( ran 𝑉 , ℝ , < ) ∈ ran 𝑉 )
59 32 38 55 57 58 syl13anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( ran 𝑉 , ℝ , < ) ∈ ran 𝑉 )
60 30 59 sseldd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( ran 𝑉 , ℝ , < ) ∈ ℕ )
61 8 60 eqeltrid ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝑁 ∈ ℕ )
62 nfcv ⊢ Ⅎ 𝑖 ℝ
63 nfcv ⊢ Ⅎ 𝑖 <
64 45 62 63 nfsup ⊢ Ⅎ 𝑖 sup ( ran 𝑉 , ℝ , < )
65 8 64 nfcxfr ⊢ Ⅎ 𝑖 𝑁
66 nfcv ⊢ Ⅎ 𝑖 (,)
67 nfcv ⊢ Ⅎ 𝑖 +∞
68 65 66 67 nfov ⊢ Ⅎ 𝑖 ( 𝑁 (,) +∞ )
69 68 nfcri ⊢ Ⅎ 𝑖 𝑟 ∈ ( 𝑁 (,) +∞ )
70 1 69 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) )
71 7 fvmpt2 ⊢ ( ( 𝑖 ∈ 𝐴 ∧ inf ( 𝑀 , ℝ , < ) ∈ ℕ ) → ( 𝑉 ‘ 𝑖 ) = inf ( 𝑀 , ℝ , < ) )
72 48 28 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) = inf ( 𝑀 , ℝ , < ) )
73 28 nnxrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( 𝑀 , ℝ , < ) ∈ ℝ* )
74 72 73 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
76 pnfxr ⊢ +∞ ∈ ℝ*
77 76 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → +∞ ∈ ℝ* )
78 elioore ⊢ ( 𝑟 ∈ ( 𝑁 (,) +∞ ) → 𝑟 ∈ ℝ )
79 78 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑟 ∈ ℝ )
80 72 28 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ∈ ℕ )
81 80 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
82 81 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
83 ne0i ⊢ ( 𝑖 ∈ 𝐴 → 𝐴 ≠ ∅ )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝐴 ≠ ∅ )
85 84 neneqd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ¬ 𝐴 = ∅ )
86 85 61 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑁 ∈ ℕ )
87 86 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑁 ∈ ℝ )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑁 ∈ ℝ )
89 85 57 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ran 𝑉 ⊆ ℝ )
90 29 56 sstrdi ⊢ ( 𝜑 → ran 𝑉 ⊆ ℝ )
91 fimaxre2 ⊢ ( ( ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥 )
92 90 37 91 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥 )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥 )
94 72 50 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ∈ ran 𝑉 )
95 suprub ⊢ ( ( ( ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥 ) ∧ ( 𝑉 ‘ 𝑖 ) ∈ ran 𝑉 ) → ( 𝑉 ‘ 𝑖 ) ≤ sup ( ran 𝑉 , ℝ , < ) )
96 89 51 93 94 95 syl31anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ≤ sup ( ran 𝑉 , ℝ , < ) )
97 96 8 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ≤ 𝑁 )
98 97 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ( 𝑉 ‘ 𝑖 ) ≤ 𝑁 )
99 88 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑁 ∈ ℝ* )
100 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑟 ∈ ( 𝑁 (,) +∞ ) )
101 ioogtlb ⊢ ( ( 𝑁 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑁 < 𝑟 )
102 99 77 100 101 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑁 < 𝑟 )
103 82 88 79 98 102 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ( 𝑉 ‘ 𝑖 ) < 𝑟 )
104 79 ltpnfd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑟 < +∞ )
105 75 77 79 103 104 eliood ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) )
106 18 26 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → inf ( 𝑀 , ℝ , < ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } )
107 72 106 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } )
108 nfcv ⊢ Ⅎ 𝑚 𝐴
109 nfrab1 ⊢ Ⅎ 𝑚 { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 }
110 6 109 nfcxfr ⊢ Ⅎ 𝑚 𝑀
111 nfcv ⊢ Ⅎ 𝑚 ℝ
112 nfcv ⊢ Ⅎ 𝑚 <
113 110 111 112 nfinf ⊢ Ⅎ 𝑚 inf ( 𝑀 , ℝ , < )
114 108 113 nfmpt ⊢ Ⅎ 𝑚 ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) )
115 7 114 nfcxfr ⊢ Ⅎ 𝑚 𝑉
116 nfcv ⊢ Ⅎ 𝑚 𝑖
117 115 116 nffv ⊢ Ⅎ 𝑚 ( 𝑉 ‘ 𝑖 )
118 117 109 nfel ⊢ Ⅎ 𝑚 ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 }
119 117 nfel1 ⊢ Ⅎ 𝑚 ( 𝑉 ‘ 𝑖 ) ∈ ℕ
120 nfcv ⊢ Ⅎ 𝑚 (,)
121 nfcv ⊢ Ⅎ 𝑚 +∞
122 117 120 121 nfov ⊢ Ⅎ 𝑚 ( ( 𝑉 ‘ 𝑖 ) (,) +∞ )
123 nfv ⊢ Ⅎ 𝑚 𝜒
124 122 123 nfralw ⊢ Ⅎ 𝑚 ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒
125 119 124 nfan ⊢ Ⅎ 𝑚 ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 )
126 118 125 nfbi ⊢ Ⅎ 𝑚 ( ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) )
127 eleq1 ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( 𝑚 ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ) )
128 eleq1 ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( 𝑚 ∈ ℕ ↔ ( 𝑉 ‘ 𝑖 ) ∈ ℕ ) )
129 oveq1 ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( 𝑚 (,) +∞ ) = ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) )
130 nfcv ⊢ Ⅎ 𝑟 ( 𝑚 (,) +∞ )
131 nfcv ⊢ Ⅎ 𝑟 𝐴
132 nfra1 ⊢ Ⅎ 𝑟 ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒
133 nfcv ⊢ Ⅎ 𝑟 ℕ
134 132 133 nfrabw ⊢ Ⅎ 𝑟 { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 }
135 6 134 nfcxfr ⊢ Ⅎ 𝑟 𝑀
136 nfcv ⊢ Ⅎ 𝑟 ℝ
137 nfcv ⊢ Ⅎ 𝑟 <
138 135 136 137 nfinf ⊢ Ⅎ 𝑟 inf ( 𝑀 , ℝ , < )
139 131 138 nfmpt ⊢ Ⅎ 𝑟 ( 𝑖 ∈ 𝐴 ↦ inf ( 𝑀 , ℝ , < ) )
140 7 139 nfcxfr ⊢ Ⅎ 𝑟 𝑉
141 nfcv ⊢ Ⅎ 𝑟 𝑖
142 140 141 nffv ⊢ Ⅎ 𝑟 ( 𝑉 ‘ 𝑖 )
143 nfcv ⊢ Ⅎ 𝑟 (,)
144 nfcv ⊢ Ⅎ 𝑟 +∞
145 142 143 144 nfov ⊢ Ⅎ 𝑟 ( ( 𝑉 ‘ 𝑖 ) (,) +∞ )
146 130 145 raleqf ⊢ ( ( 𝑚 (,) +∞ ) = ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) → ( ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 ↔ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) )
147 129 146 syl ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 ↔ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) )
148 128 147 anbi12d ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( ( 𝑚 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) ) )
149 127 148 bibi12d ⊢ ( 𝑚 = ( 𝑉 ‘ 𝑖 ) → ( ( 𝑚 ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( 𝑚 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 ) ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) ) ) )
150 rabid ⊢ ( 𝑚 ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( 𝑚 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 ) )
151 117 126 149 150 vtoclgf ⊢ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ → ( ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) ) )
152 80 151 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑉 ‘ 𝑖 ) ∈ { 𝑚 ∈ ℕ ∣ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) 𝜒 } ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) ) )
153 107 152 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ℕ ∧ ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 ) )
154 153 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∀ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) 𝜒 )
155 154 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) +∞ ) ) → 𝜒 )
156 105 155 syldan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → 𝜒 )
157 156 an32s ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) ∧ 𝑖 ∈ 𝐴 ) → 𝜒 )
158 157 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ( 𝑖 ∈ 𝐴 → 𝜒 ) )
159 70 158 ralrimi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑁 (,) +∞ ) ) → ∀ 𝑖 ∈ 𝐴 𝜒 )
160 159 ex ⊢ ( 𝜑 → ( 𝑟 ∈ ( 𝑁 (,) +∞ ) → ∀ 𝑖 ∈ 𝐴 𝜒 ) )
161 2 160 ralrimi ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( 𝑁 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
162 161 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∀ 𝑟 ∈ ( 𝑁 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
163 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 (,) +∞ ) = ( 𝑁 (,) +∞ ) )
164 nfcv ⊢ Ⅎ 𝑟 ( 𝑛 (,) +∞ )
165 140 nfrn ⊢ Ⅎ 𝑟 ran 𝑉
166 165 136 137 nfsup ⊢ Ⅎ 𝑟 sup ( ran 𝑉 , ℝ , < )
167 8 166 nfcxfr ⊢ Ⅎ 𝑟 𝑁
168 167 143 144 nfov ⊢ Ⅎ 𝑟 ( 𝑁 (,) +∞ )
169 164 168 raleqf ⊢ ( ( 𝑛 (,) +∞ ) = ( 𝑁 (,) +∞ ) → ( ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ↔ ∀ 𝑟 ∈ ( 𝑁 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ) )
170 163 169 syl ⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ↔ ∀ 𝑟 ∈ ( 𝑁 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ) )
171 170 rspcev ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 𝑁 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
172 61 162 171 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )
173 16 172 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑟 ∈ ( 𝑛 (,) +∞ ) ∀ 𝑖 ∈ 𝐴 𝜒 )