# 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 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
fourierdlem31.r ${⊢}Ⅎ{r}\phantom{\rule{.4em}{0ex}}{\phi }$
fourierdlem31.iv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{V}$
fourierdlem31.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fourierdlem31.exm ${⊢}{\phi }\to \forall {i}\in {A}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {r}\in \left({m},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{\chi }$
fourierdlem31.m ${⊢}{M}=\left\{{m}\in ℕ|\forall {r}\in \left({m},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{\chi }\right\}$
fourierdlem31.v ${⊢}{V}=\left({i}\in {A}⟼sup\left({M},ℝ,<\right)\right)$
fourierdlem31.n ${⊢}{N}=sup\left(\mathrm{ran}{V},ℝ,<\right)$
Assertion fourierdlem31 ${⊢}{\phi }\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {r}\in \left({n},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }$

### Proof

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