# Metamath Proof Explorer

## Theorem bndth

Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -u F .) (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 ${⊢}{X}=\bigcup {J}$
bndth.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
bndth.3 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
bndth.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
Assertion bndth ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}$

### Proof

Step Hyp Ref Expression
1 bndth.1 ${⊢}{X}=\bigcup {J}$
2 bndth.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 bndth.3 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
4 bndth.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
5 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
6 2 5 eqeltri ${⊢}{K}\in \mathrm{TopOn}\left(ℝ\right)$
7 6 toponunii ${⊢}ℝ=\bigcup {K}$
8 1 7 cnf ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}:{X}⟶ℝ$
9 4 8 syl ${⊢}{\phi }\to {F}:{X}⟶ℝ$
10 9 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq ℝ$
11 unieq ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \bigcup {u}=\bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
12 imassrn ${⊢}\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq \mathrm{ran}\left(.\right)$
13 12 unissi ${⊢}\bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq \bigcup \mathrm{ran}\left(.\right)$
14 unirnioo ${⊢}ℝ=\bigcup \mathrm{ran}\left(.\right)$
15 13 14 sseqtrri ${⊢}\bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq ℝ$
16 id ${⊢}{x}\in ℝ\to {x}\in ℝ$
17 ltp1 ${⊢}{x}\in ℝ\to {x}<{x}+1$
18 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
19 peano2re ${⊢}{x}\in ℝ\to {x}+1\in ℝ$
20 18 19 sseldi ${⊢}{x}\in ℝ\to {x}+1\in {ℝ}^{*}$
21 elioomnf ${⊢}{x}+1\in {ℝ}^{*}\to \left({x}\in \left(\mathrm{-\infty },{x}+1\right)↔\left({x}\in ℝ\wedge {x}<{x}+1\right)\right)$
22 20 21 syl ${⊢}{x}\in ℝ\to \left({x}\in \left(\mathrm{-\infty },{x}+1\right)↔\left({x}\in ℝ\wedge {x}<{x}+1\right)\right)$
23 16 17 22 mpbir2and ${⊢}{x}\in ℝ\to {x}\in \left(\mathrm{-\infty },{x}+1\right)$
24 df-ov ${⊢}\left(\mathrm{-\infty },{x}+1\right)=\left(.\right)\left(⟨\mathrm{-\infty },{x}+1⟩\right)$
25 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
26 25 elexi ${⊢}\mathrm{-\infty }\in \mathrm{V}$
27 26 snid ${⊢}\mathrm{-\infty }\in \left\{\mathrm{-\infty }\right\}$
28 opelxpi ${⊢}\left(\mathrm{-\infty }\in \left\{\mathrm{-\infty }\right\}\wedge {x}+1\in ℝ\right)\to ⟨\mathrm{-\infty },{x}+1⟩\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)$
29 27 19 28 sylancr ${⊢}{x}\in ℝ\to ⟨\mathrm{-\infty },{x}+1⟩\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)$
30 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
31 ffun ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \mathrm{Fun}\left(.\right)$
32 30 31 ax-mp ${⊢}\mathrm{Fun}\left(.\right)$
33 snssi ${⊢}\mathrm{-\infty }\in {ℝ}^{*}\to \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
34 25 33 ax-mp ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
35 xpss12 ${⊢}\left(\left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\wedge ℝ\subseteq {ℝ}^{*}\right)\to \left\{\mathrm{-\infty }\right\}×ℝ\subseteq {ℝ}^{*}×{ℝ}^{*}$
36 34 18 35 mp2an ${⊢}\left\{\mathrm{-\infty }\right\}×ℝ\subseteq {ℝ}^{*}×{ℝ}^{*}$
37 30 fdmi ${⊢}\mathrm{dom}\left(.\right)={ℝ}^{*}×{ℝ}^{*}$
38 36 37 sseqtrri ${⊢}\left\{\mathrm{-\infty }\right\}×ℝ\subseteq \mathrm{dom}\left(.\right)$
39 funfvima2 ${⊢}\left(\mathrm{Fun}\left(.\right)\wedge \left\{\mathrm{-\infty }\right\}×ℝ\subseteq \mathrm{dom}\left(.\right)\right)\to \left(⟨\mathrm{-\infty },{x}+1⟩\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\to \left(.\right)\left(⟨\mathrm{-\infty },{x}+1⟩\right)\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\right)$
40 32 38 39 mp2an ${⊢}⟨\mathrm{-\infty },{x}+1⟩\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\to \left(.\right)\left(⟨\mathrm{-\infty },{x}+1⟩\right)\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
41 29 40 syl ${⊢}{x}\in ℝ\to \left(.\right)\left(⟨\mathrm{-\infty },{x}+1⟩\right)\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
42 24 41 eqeltrid ${⊢}{x}\in ℝ\to \left(\mathrm{-\infty },{x}+1\right)\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
43 elunii ${⊢}\left({x}\in \left(\mathrm{-\infty },{x}+1\right)\wedge \left(\mathrm{-\infty },{x}+1\right)\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\right)\to {x}\in \bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
44 23 42 43 syl2anc ${⊢}{x}\in ℝ\to {x}\in \bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
45 44 ssriv ${⊢}ℝ\subseteq \bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
46 15 45 eqssi ${⊢}\bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]=ℝ$
47 11 46 eqtrdi ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \bigcup {u}=ℝ$
48 47 sseq2d ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \left(\mathrm{ran}{F}\subseteq \bigcup {u}↔\mathrm{ran}{F}\subseteq ℝ\right)$
49 pweq ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to 𝒫{u}=𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
50 49 ineq1d ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to 𝒫{u}\cap \mathrm{Fin}=𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}$
51 50 rexeqdv ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \left(\exists {v}\in \left(𝒫{u}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}↔\exists {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)$
52 48 51 imbi12d ${⊢}{u}=\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \left(\left(\mathrm{ran}{F}\subseteq \bigcup {u}\to \exists {v}\in \left(𝒫{u}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)↔\left(\mathrm{ran}{F}\subseteq ℝ\to \exists {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)$
53 rncmp ${⊢}\left({J}\in \mathrm{Comp}\wedge {F}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {K}{↾}_{𝑡}\mathrm{ran}{F}\in \mathrm{Comp}$
54 3 4 53 syl2anc ${⊢}{\phi }\to {K}{↾}_{𝑡}\mathrm{ran}{F}\in \mathrm{Comp}$
55 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
56 2 55 eqeltri ${⊢}{K}\in \mathrm{Top}$
57 7 cmpsub ${⊢}\left({K}\in \mathrm{Top}\wedge \mathrm{ran}{F}\subseteq ℝ\right)\to \left({K}{↾}_{𝑡}\mathrm{ran}{F}\in \mathrm{Comp}↔\forall {u}\in 𝒫{K}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{F}\subseteq \bigcup {u}\to \exists {v}\in \left(𝒫{u}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)$
58 56 10 57 sylancr ${⊢}{\phi }\to \left({K}{↾}_{𝑡}\mathrm{ran}{F}\in \mathrm{Comp}↔\forall {u}\in 𝒫{K}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{F}\subseteq \bigcup {u}\to \exists {v}\in \left(𝒫{u}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)$
59 54 58 mpbid ${⊢}{\phi }\to \forall {u}\in 𝒫{K}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{F}\subseteq \bigcup {u}\to \exists {v}\in \left(𝒫{u}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)$
60 retopbas ${⊢}\mathrm{ran}\left(.\right)\in \mathrm{TopBases}$
61 bastg ${⊢}\mathrm{ran}\left(.\right)\in \mathrm{TopBases}\to \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
62 60 61 ax-mp ${⊢}\mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
63 62 2 sseqtrri ${⊢}\mathrm{ran}\left(.\right)\subseteq {K}$
64 12 63 sstri ${⊢}\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq {K}$
65 56 64 elpwi2 ${⊢}\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\in 𝒫{K}$
66 65 a1i ${⊢}{\phi }\to \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\in 𝒫{K}$
67 52 59 66 rspcdva ${⊢}{\phi }\to \left(\mathrm{ran}{F}\subseteq ℝ\to \exists {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}\right)$
68 10 67 mpd ${⊢}{\phi }\to \exists {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}\subseteq \bigcup {v}$
69 simpr ${⊢}\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\to {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)$
70 elin ${⊢}{v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)↔\left({v}\in 𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\wedge {v}\in \mathrm{Fin}\right)$
71 69 70 sylib ${⊢}\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\to \left({v}\in 𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\wedge {v}\in \mathrm{Fin}\right)$
72 71 adantrr ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to \left({v}\in 𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\wedge {v}\in \mathrm{Fin}\right)$
73 72 simprd ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to {v}\in \mathrm{Fin}$
74 71 simpld ${⊢}\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\to {v}\in 𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
75 74 elpwid ${⊢}\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\to {v}\subseteq \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
76 34 sseli ${⊢}{u}\in \left\{\mathrm{-\infty }\right\}\to {u}\in {ℝ}^{*}$
77 76 adantr ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to {u}\in {ℝ}^{*}$
78 18 sseli ${⊢}{w}\in ℝ\to {w}\in {ℝ}^{*}$
79 78 adantl ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to {w}\in {ℝ}^{*}$
80 mnflt ${⊢}{w}\in ℝ\to \mathrm{-\infty }<{w}$
81 xrltnle ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }<{w}↔¬{w}\le \mathrm{-\infty }\right)$
82 25 78 81 sylancr ${⊢}{w}\in ℝ\to \left(\mathrm{-\infty }<{w}↔¬{w}\le \mathrm{-\infty }\right)$
83 80 82 mpbid ${⊢}{w}\in ℝ\to ¬{w}\le \mathrm{-\infty }$
84 83 adantl ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to ¬{w}\le \mathrm{-\infty }$
85 elsni ${⊢}{u}\in \left\{\mathrm{-\infty }\right\}\to {u}=\mathrm{-\infty }$
86 85 adantr ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to {u}=\mathrm{-\infty }$
87 86 breq2d ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to \left({w}\le {u}↔{w}\le \mathrm{-\infty }\right)$
88 84 87 mtbird ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to ¬{w}\le {u}$
89 ioo0 ${⊢}\left({u}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({u},{w}\right)=\varnothing ↔{w}\le {u}\right)$
90 76 78 89 syl2an ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to \left(\left({u},{w}\right)=\varnothing ↔{w}\le {u}\right)$
91 90 necon3abid ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to \left(\left({u},{w}\right)\ne \varnothing ↔¬{w}\le {u}\right)$
92 88 91 mpbird ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to \left({u},{w}\right)\ne \varnothing$
93 df-ioo ${⊢}\left(.\right)=\left({y}\in {ℝ}^{*},{z}\in {ℝ}^{*}⟼\left\{{v}\in {ℝ}^{*}|\left({y}<{v}\wedge {v}<{z}\right)\right\}\right)$
94 idd ${⊢}\left({x}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({x}<{w}\to {x}<{w}\right)$
95 xrltle ${⊢}\left({x}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({x}<{w}\to {x}\le {w}\right)$
96 idd ${⊢}\left({u}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({u}<{x}\to {u}<{x}\right)$
97 xrltle ${⊢}\left({u}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left({u}<{x}\to {u}\le {x}\right)$
98 93 94 95 96 97 ixxub ${⊢}\left({u}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\wedge \left({u},{w}\right)\ne \varnothing \right)\to sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)={w}$
99 77 79 92 98 syl3anc ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)={w}$
100 simpr ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to {w}\in ℝ$
101 99 100 eqeltrd ${⊢}\left({u}\in \left\{\mathrm{-\infty }\right\}\wedge {w}\in ℝ\right)\to sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)\in ℝ$
102 101 rgen2 ${⊢}\forall {u}\in \left\{\mathrm{-\infty }\right\}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)\in ℝ$
103 fveq2 ${⊢}{z}=⟨{u},{w}⟩\to \left(.\right)\left({z}\right)=\left(.\right)\left(⟨{u},{w}⟩\right)$
104 df-ov ${⊢}\left({u},{w}\right)=\left(.\right)\left(⟨{u},{w}⟩\right)$
105 103 104 eqtr4di ${⊢}{z}=⟨{u},{w}⟩\to \left(.\right)\left({z}\right)=\left({u},{w}\right)$
106 105 supeq1d ${⊢}{z}=⟨{u},{w}⟩\to sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)=sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)$
107 106 eleq1d ${⊢}{z}=⟨{u},{w}⟩\to \left(sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ↔sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)\in ℝ\right)$
108 107 ralxp ${⊢}\forall {z}\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\phantom{\rule{.4em}{0ex}}sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ↔\forall {u}\in \left\{\mathrm{-\infty }\right\}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}sup\left(\left({u},{w}\right),{ℝ}^{*},<\right)\in ℝ$
109 102 108 mpbir ${⊢}\forall {z}\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\phantom{\rule{.4em}{0ex}}sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ$
110 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
111 30 110 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
112 supeq1 ${⊢}{w}=\left(.\right)\left({z}\right)\to sup\left({w},{ℝ}^{*},<\right)=sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)$
113 112 eleq1d ${⊢}{w}=\left(.\right)\left({z}\right)\to \left(sup\left({w},{ℝ}^{*},<\right)\in ℝ↔sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ\right)$
114 113 ralima ${⊢}\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge \left\{\mathrm{-\infty }\right\}×ℝ\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to \left(\forall {w}\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ↔\forall {z}\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\phantom{\rule{.4em}{0ex}}sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ\right)$
115 111 36 114 mp2an ${⊢}\forall {w}\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ↔\forall {z}\in \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\phantom{\rule{.4em}{0ex}}sup\left(\left(.\right)\left({z}\right),{ℝ}^{*},<\right)\in ℝ$
116 109 115 mpbir ${⊢}\forall {w}\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ$
117 ssralv ${⊢}{v}\subseteq \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\to \left(\forall {w}\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ\to \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ\right)$
118 75 116 117 mpisyl ${⊢}\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\to \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ$
119 118 adantrr ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ$
120 fimaxre3 ${⊢}\left({v}\in \mathrm{Fin}\wedge \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\in ℝ\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}$
121 73 119 120 syl2anc ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}$
122 simplrr ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \mathrm{ran}{F}\subseteq \bigcup {v}$
123 122 sselda ${⊢}\left(\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\wedge {z}\in \mathrm{ran}{F}\right)\to {z}\in \bigcup {v}$
124 eluni2 ${⊢}{z}\in \bigcup {v}↔\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in {w}$
125 r19.29r ${⊢}\left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in {w}\wedge \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to \exists {w}\in {v}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)$
126 sspwuni ${⊢}\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq 𝒫ℝ↔\bigcup \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq ℝ$
127 15 126 mpbir ${⊢}\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\subseteq 𝒫ℝ$
128 75 3ad2ant1 ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {v}\subseteq \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
129 simp2r ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {w}\in {v}$
130 128 129 sseldd ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {w}\in \left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]$
131 127 130 sseldi ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {w}\in 𝒫ℝ$
132 131 elpwid ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {w}\subseteq ℝ$
133 simp3l ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {z}\in {w}$
134 132 133 sseldd ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {z}\in ℝ$
135 118 r19.21bi ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge {w}\in {v}\right)\to sup\left({w},{ℝ}^{*},<\right)\in ℝ$
136 135 adantrl ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\right)\to sup\left({w},{ℝ}^{*},<\right)\in ℝ$
137 136 3adant3 ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to sup\left({w},{ℝ}^{*},<\right)\in ℝ$
138 simp2l ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {x}\in ℝ$
139 132 18 sstrdi ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {w}\subseteq {ℝ}^{*}$
140 supxrub ${⊢}\left({w}\subseteq {ℝ}^{*}\wedge {z}\in {w}\right)\to {z}\le sup\left({w},{ℝ}^{*},<\right)$
141 139 133 140 syl2anc ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {z}\le sup\left({w},{ℝ}^{*},<\right)$
142 simp3r ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to sup\left({w},{ℝ}^{*},<\right)\le {x}$
143 134 137 138 141 142 letrd ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\wedge \left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\right)\to {z}\le {x}$
144 143 3expia ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge \left({x}\in ℝ\wedge {w}\in {v}\right)\right)\to \left(\left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to {z}\le {x}\right)$
145 144 anassrs ${⊢}\left(\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge {x}\in ℝ\right)\wedge {w}\in {v}\right)\to \left(\left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to {z}\le {x}\right)$
146 145 rexlimdva ${⊢}\left(\left({\phi }\wedge {v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\right)\wedge {x}\in ℝ\right)\to \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to {z}\le {x}\right)$
147 146 adantlrr ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to {z}\le {x}\right)$
148 125 147 syl5 ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \left(\left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in {w}\wedge \forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\right)\to {z}\le {x}\right)$
149 148 expdimp ${⊢}\left(\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\wedge \exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in {w}\right)\to \left(\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to {z}\le {x}\right)$
150 124 149 sylan2b ${⊢}\left(\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\wedge {z}\in \bigcup {v}\right)\to \left(\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to {z}\le {x}\right)$
151 123 150 syldan ${⊢}\left(\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\wedge {z}\in \mathrm{ran}{F}\right)\to \left(\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to {z}\le {x}\right)$
152 151 ralrimdva ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \left(\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to \forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
153 9 ffnd ${⊢}{\phi }\to {F}Fn{X}$
154 153 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to {F}Fn{X}$
155 breq1 ${⊢}{z}={F}\left({y}\right)\to \left({z}\le {x}↔{F}\left({y}\right)\le {x}\right)$
156 155 ralrn ${⊢}{F}Fn{X}\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
157 154 156 syl ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
158 152 157 sylibd ${⊢}\left(\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\wedge {x}\in ℝ\right)\to \left(\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
159 158 reximdva ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {v}\phantom{\rule{.4em}{0ex}}sup\left({w},{ℝ}^{*},<\right)\le {x}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
160 121 159 mpd ${⊢}\left({\phi }\wedge \left({v}\in \left(𝒫\left(.\right)\left[\left\{\mathrm{-\infty }\right\}×ℝ\right]\cap \mathrm{Fin}\right)\wedge \mathrm{ran}{F}\subseteq \bigcup {v}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}$
161 68 160 rexlimddv ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}$