# Metamath Proof Explorer

## Theorem ssfiunibd

Description: A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ssfiunibd.fi ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
ssfiunibd.b ${⊢}\left({\phi }\wedge {z}\in \bigcup {A}\right)\to {B}\in ℝ$
ssfiunibd.bd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
ssfiunibd.ssun ${⊢}{\phi }\to {C}\subseteq \bigcup {A}$
Assertion ssfiunibd ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{B}\le {w}$

### Proof

Step Hyp Ref Expression
1 ssfiunibd.fi ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 ssfiunibd.b ${⊢}\left({\phi }\wedge {z}\in \bigcup {A}\right)\to {B}\in ℝ$
3 ssfiunibd.bd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
4 ssfiunibd.ssun ${⊢}{\phi }\to {C}\subseteq \bigcup {A}$
5 simpll ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\right)\to {\phi }$
6 19.8a ${⊢}\left({z}\in {x}\wedge {x}\in {A}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\wedge {x}\in {A}\right)$
7 6 ancoms ${⊢}\left({x}\in {A}\wedge {z}\in {x}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\wedge {x}\in {A}\right)$
8 eluni ${⊢}{z}\in \bigcup {A}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\wedge {x}\in {A}\right)$
9 7 8 sylibr ${⊢}\left({x}\in {A}\wedge {z}\in {x}\right)\to {z}\in \bigcup {A}$
10 9 adantll ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\right)\to {z}\in \bigcup {A}$
11 5 10 2 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\right)\to {B}\in ℝ$
12 eqid ${⊢}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)=if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)$
13 11 3 12 upbdrech2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\in ℝ\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\right)$
14 13 simpld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\in ℝ$
15 14 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\in ℝ$
16 fimaxre3 ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\in ℝ\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
17 1 15 16 syl2anc ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
18 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {w}\in ℝ\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{A}$
20 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{x}=\varnothing$
21 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}0$
22 nfre1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}$
23 22 nfab ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
24 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}ℝ$
25 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}<$
26 23 24 25 nfsup ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
27 20 21 26 nfif ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)$
28 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\le$
29 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{w}$
30 27 28 29 nfbr ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
31 19 30 nfralw ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
32 18 31 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)$
33 4 sselda ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to {z}\in \bigcup {A}$
34 33 8 sylib ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\wedge {x}\in {A}\right)$
35 exancom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\wedge {x}\in {A}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {z}\in {x}\right)$
36 34 35 sylib ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {z}\in {x}\right)$
37 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {z}\in {x}\right)$
38 36 37 sylibr ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {x}$
39 38 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {z}\in {C}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {x}$
40 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {w}\in ℝ\right)$
41 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
42 40 41 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)$
43 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
44 42 43 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {z}\in {C}\right)$
45 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}\le {w}$
46 11 3impa ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\in ℝ$
47 46 3adant1r ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\in ℝ$
48 47 3adant1r ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\in ℝ$
49 n0i ${⊢}{z}\in {x}\to ¬{x}=\varnothing$
50 49 adantl ${⊢}\left({x}\in {A}\wedge {z}\in {x}\right)\to ¬{x}=\varnothing$
51 50 iffalsed ${⊢}\left({x}\in {A}\wedge {z}\in {x}\right)\to if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)=sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
52 51 eqcomd ${⊢}\left({x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)=if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)$
53 52 3adant1 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)=if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)$
54 14 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\in ℝ$
55 53 54 eqeltrd ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\in ℝ$
56 55 3adant1r ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\in ℝ$
57 56 3adant1r ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\in ℝ$
58 simp1lr ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {w}\in ℝ$
59 nfv ${⊢}Ⅎ{u}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {A}\right)$
60 nfab1 ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
61 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}ℝ$
62 abid ${⊢}{u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}↔\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}$
63 62 biimpi ${⊢}{u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\to \exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}$
64 63 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}$
65 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {A}\right)$
66 22 nfsab ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
67 65 66 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)$
68 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{u}\in ℝ$
69 simp3 ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\wedge {u}={B}\right)\to {u}={B}$
70 11 3adant3 ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\wedge {u}={B}\right)\to {B}\in ℝ$
71 69 70 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {z}\in {x}\wedge {u}={B}\right)\to {u}\in ℝ$
72 71 3exp ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({z}\in {x}\to \left({u}={B}\to {u}\in ℝ\right)\right)$
73 72 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \left({z}\in {x}\to \left({u}={B}\to {u}\in ℝ\right)\right)$
74 67 68 73 rexlimd ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \left(\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\to {u}\in ℝ\right)$
75 64 74 mpd ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to {u}\in ℝ$
76 75 ex ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({u}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\to {u}\in ℝ\right)$
77 59 60 61 76 ssrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\subseteq ℝ$
78 77 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\subseteq ℝ$
79 simp3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {z}\in {x}$
80 elabrexg ${⊢}\left({z}\in {x}\wedge {B}\in ℝ\right)\to {B}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
81 79 46 80 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
82 81 ne0d ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\ne \varnothing$
83 abid ${⊢}{v}\in \left\{{v}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}\right\}↔\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}$
84 83 biimpi ${⊢}{v}\in \left\{{v}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}\right\}\to \exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}$
85 eqeq1 ${⊢}{u}={v}\to \left({u}={B}↔{v}={B}\right)$
86 85 rexbidv ${⊢}{u}={v}\to \left(\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}↔\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}\right)$
87 86 cbvabv ${⊢}\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}=\left\{{v}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}\right\}$
88 84 87 eleq2s ${⊢}{v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\to \exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}$
89 88 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\wedge {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}$
90 nfra1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
91 65 90 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)$
92 22 nfsab ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}$
93 91 92 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\wedge {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)$
94 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{v}\le {y}$
95 simp3 ${⊢}\left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\wedge {z}\in {x}\wedge {v}={B}\right)\to {v}={B}$
96 rspa ${⊢}\left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\wedge {z}\in {x}\right)\to {B}\le {y}$
97 96 3adant3 ${⊢}\left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\wedge {z}\in {x}\wedge {v}={B}\right)\to {B}\le {y}$
98 95 97 eqbrtrd ${⊢}\left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\wedge {z}\in {x}\wedge {v}={B}\right)\to {v}\le {y}$
99 98 3exp ${⊢}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\to \left({z}\in {x}\to \left({v}={B}\to {v}\le {y}\right)\right)$
100 99 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\to \left({z}\in {x}\to \left({v}={B}\to {v}\le {y}\right)\right)$
101 100 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\wedge {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \left({z}\in {x}\to \left({v}={B}\to {v}\le {y}\right)\right)$
102 93 94 101 rexlimd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\wedge {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to \left(\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{v}={B}\to {v}\le {y}\right)$
103 89 102 mpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\wedge {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to {v}\le {y}$
104 103 ralrimiva ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\right)\to \forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}$
105 104 ex ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\to \forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}\right)$
106 105 reximdv ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{B}\le {y}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}\right)$
107 3 106 mpd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}$
108 107 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}$
109 suprub ${⊢}\left(\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\subseteq ℝ\wedge \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {v}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\phantom{\rule{.4em}{0ex}}{v}\le {y}\right)\wedge {B}\in \left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\}\right)\to {B}\le sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
110 78 82 108 81 109 syl31anc ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\le sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
111 110 3adant1r ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\le sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
112 111 3adant1r ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\le sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)$
113 52 3adant1 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)=if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)$
114 rspa ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\wedge {x}\in {A}\right)\to if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
115 114 3adant3 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\wedge {x}\in {A}\wedge {z}\in {x}\right)\to if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}$
116 113 115 eqbrtrd ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\le {w}$
117 116 3adant1l ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\le {w}$
118 48 57 58 112 117 letrd ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {x}\in {A}\wedge {z}\in {x}\right)\to {B}\le {w}$
119 118 3exp ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\to \left({x}\in {A}\to \left({z}\in {x}\to {B}\le {w}\right)\right)$
120 119 adantr ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {z}\in {C}\right)\to \left({x}\in {A}\to \left({z}\in {x}\to {B}\le {w}\right)\right)$
121 44 45 120 rexlimd ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {z}\in {C}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {x}\to {B}\le {w}\right)$
122 39 121 mpd ${⊢}\left(\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\wedge {z}\in {C}\right)\to {B}\le {w}$
123 122 ex ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\to \left({z}\in {C}\to {B}\le {w}\right)$
124 32 123 ralrimi ${⊢}\left(\left({\phi }\wedge {w}\in ℝ\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{B}\le {w}$
125 124 ex ${⊢}\left({\phi }\wedge {w}\in ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{B}\le {w}\right)$
126 125 reximdva ${⊢}{\phi }\to \left(\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({x}=\varnothing ,0,sup\left(\left\{{u}|\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{u}={B}\right\},ℝ,<\right)\right)\le {w}\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{B}\le {w}\right)$
127 17 126 mpd ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{B}\le {w}$