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