# Metamath Proof Explorer

## Theorem elovolmr

Description: Sufficient condition for elementhood in the set M . (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypotheses elovolm.1 ${⊢}{M}=\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right\}$
elovolmr.2 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
Assertion elovolmr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {M}$

### Proof

Step Hyp Ref Expression
1 elovolm.1 ${⊢}{M}=\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right\}$
2 elovolmr.2 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
3 elovolmlem ${⊢}{F}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}:ℕ⟶\le \cap {ℝ}^{2}$
4 id ${⊢}{f}={F}\to {f}={F}$
5 4 eqcomd ${⊢}{f}={F}\to {F}={f}$
6 5 coeq2d ${⊢}{f}={F}\to \left(\mathrm{abs}\circ -\right)\circ {F}=\left(\mathrm{abs}\circ -\right)\circ {f}$
7 6 seqeq3d ${⊢}{f}={F}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
8 2 7 syl5eq ${⊢}{f}={F}\to {S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
9 8 rneqd ${⊢}{f}={F}\to \mathrm{ran}{S}=\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
10 9 supeq1d ${⊢}{f}={F}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)$
11 10 biantrud ${⊢}{f}={F}\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)$
12 coeq2 ${⊢}{f}={F}\to \left(.\right)\circ {f}=\left(.\right)\circ {F}$
13 12 rneqd ${⊢}{f}={F}\to \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\mathrm{ran}\left(\left(.\right)\circ {F}\right)$
14 13 unieqd ${⊢}{f}={F}\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
15 14 sseq2d ${⊢}{f}={F}\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
16 11 15 bitr3d ${⊢}{f}={F}\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
17 16 rspcev ${⊢}\left({F}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to \exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$
18 3 17 sylanbr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to \exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$
19 1 elovolm ${⊢}sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {M}↔\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$
20 18 19 sylibr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {M}$