# Metamath Proof Explorer

## Theorem filbcmb

Description: Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion filbcmb ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 reex ${⊢}ℝ\in \mathrm{V}$
2 1 ssex ${⊢}{B}\subseteq ℝ\to {B}\in \mathrm{V}$
3 indexfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)$
4 3 3expia ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{V}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)$
5 2 4 sylan2 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)$
6 5 3adant2 ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)$
7 r19.2z ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
8 rexn0 ${⊢}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {w}\ne \varnothing$
9 8 rexlimivw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {w}\ne \varnothing$
10 7 9 syl ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to {w}\ne \varnothing$
11 10 ex ${⊢}{A}\ne \varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {w}\ne \varnothing \right)$
12 11 3ad2ant2 ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {w}\ne \varnothing \right)$
13 12 ad2antrr ${⊢}\left(\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\wedge {w}\subseteq {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {w}\ne \varnothing \right)$
14 sstr ${⊢}\left({w}\subseteq {B}\wedge {B}\subseteq ℝ\right)\to {w}\subseteq ℝ$
15 14 ancoms ${⊢}\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\to {w}\subseteq ℝ$
16 fimaxre ${⊢}\left({w}\subseteq ℝ\wedge {w}\in \mathrm{Fin}\wedge {w}\ne \varnothing \right)\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}$
17 16 3expia ${⊢}\left({w}\subseteq ℝ\wedge {w}\in \mathrm{Fin}\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
18 15 17 sylan ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge {w}\in \mathrm{Fin}\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
19 18 anasss ${⊢}\left({B}\subseteq ℝ\wedge \left({w}\subseteq {B}\wedge {w}\in \mathrm{Fin}\right)\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
20 19 ancom2s ${⊢}\left({B}\subseteq ℝ\wedge \left({w}\in \mathrm{Fin}\wedge {w}\subseteq {B}\right)\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
21 20 3ad2antl3 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge \left({w}\in \mathrm{Fin}\wedge {w}\subseteq {B}\right)\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
22 21 anassrs ${⊢}\left(\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\wedge {w}\subseteq {B}\right)\to \left({w}\ne \varnothing \to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
23 13 22 syld ${⊢}\left(\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\wedge {w}\subseteq {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
24 23 a1dd ${⊢}\left(\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\wedge {w}\subseteq {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \left(\forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)$
25 24 ex ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\to \left({w}\subseteq {B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \left(\forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\right)$
26 25 3impd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\to \left(\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
27 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)$
28 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
29 nfre1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
30 28 29 nfralw ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
31 27 30 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)$
32 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)$
33 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{A}$
34 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{w}$
35 nfra1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
36 34 35 nfrex ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
37 33 36 nfralw ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)$
38 32 37 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)$
39 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)$
40 38 39 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)$
41 breq1 ${⊢}{y}={v}\to \left({y}\le {z}↔{v}\le {z}\right)$
42 41 imbi1d ${⊢}{y}={v}\to \left(\left({y}\le {z}\to {\phi }\right)↔\left({v}\le {z}\to {\phi }\right)\right)$
43 42 ralbidv ${⊢}{y}={v}\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)\right)$
44 43 cbvrexvw ${⊢}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)↔\exists {v}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)$
45 rsp ${⊢}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)\to \left({z}\in {B}\to \left({v}\le {z}\to {\phi }\right)\right)$
46 ssel2 ${⊢}\left({w}\subseteq {B}\wedge {v}\in {w}\right)\to {v}\in {B}$
47 ssel2 ${⊢}\left({B}\subseteq ℝ\wedge {v}\in {B}\right)\to {v}\in ℝ$
48 46 47 sylan2 ${⊢}\left({B}\subseteq ℝ\wedge \left({w}\subseteq {B}\wedge {v}\in {w}\right)\right)\to {v}\in ℝ$
49 48 anassrs ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge {v}\in {w}\right)\to {v}\in ℝ$
50 49 adantlr ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge {v}\in {w}\right)\to {v}\in ℝ$
51 50 adantlr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {v}\in ℝ$
52 ssel2 ${⊢}\left({w}\subseteq {B}\wedge {y}\in {w}\right)\to {y}\in {B}$
53 ssel2 ${⊢}\left({B}\subseteq ℝ\wedge {y}\in {B}\right)\to {y}\in ℝ$
54 52 53 sylan2 ${⊢}\left({B}\subseteq ℝ\wedge \left({w}\subseteq {B}\wedge {y}\in {w}\right)\right)\to {y}\in ℝ$
55 54 anassrs ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge {y}\in {w}\right)\to {y}\in ℝ$
56 55 adantrr ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\to {y}\in ℝ$
57 56 ad2antrr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {y}\in ℝ$
58 ssel2 ${⊢}\left({B}\subseteq ℝ\wedge {z}\in {B}\right)\to {z}\in ℝ$
59 58 adantlr ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge {z}\in {B}\right)\to {z}\in ℝ$
60 59 ad2ant2r ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\to {z}\in ℝ$
61 60 adantr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {z}\in ℝ$
62 breq1 ${⊢}{u}={v}\to \left({u}\le {y}↔{v}\le {y}\right)$
63 62 rspccva ${⊢}\left(\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\wedge {v}\in {w}\right)\to {v}\le {y}$
64 63 adantll ${⊢}\left(\left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\wedge {v}\in {w}\right)\to {v}\le {y}$
65 64 adantll ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge {v}\in {w}\right)\to {v}\le {y}$
66 65 adantlr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {v}\le {y}$
67 simplrr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {y}\le {z}$
68 51 57 61 66 67 letrd ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to {v}\le {z}$
69 pm2.27 ${⊢}{z}\in {B}\to \left(\left({z}\in {B}\to \left({v}\le {z}\to {\phi }\right)\right)\to \left({v}\le {z}\to {\phi }\right)\right)$
70 69 adantr ${⊢}\left({z}\in {B}\wedge {y}\le {z}\right)\to \left(\left({z}\in {B}\to \left({v}\le {z}\to {\phi }\right)\right)\to \left({v}\le {z}\to {\phi }\right)\right)$
71 70 ad2antlr ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to \left(\left({z}\in {B}\to \left({v}\le {z}\to {\phi }\right)\right)\to \left({v}\le {z}\to {\phi }\right)\right)$
72 68 71 mpid ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to \left(\left({z}\in {B}\to \left({v}\le {z}\to {\phi }\right)\right)\to {\phi }\right)$
73 45 72 syl5 ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {v}\in {w}\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)\to {\phi }\right)$
74 73 adantlr ${⊢}\left(\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {x}\in {A}\right)\wedge {v}\in {w}\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)\to {\phi }\right)$
75 74 rexlimdva ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {x}\in {A}\right)\to \left(\exists {v}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({v}\le {z}\to {\phi }\right)\to {\phi }\right)$
76 44 75 syl5bi ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge {x}\in {A}\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to {\phi }\right)$
77 76 ralimdva ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
78 77 imp ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
79 78 an32s ${⊢}\left(\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\wedge \left({z}\in {B}\wedge {y}\le {z}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
80 79 exp32 ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left({z}\in {B}\to \left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
81 80 an32s ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\to \left({z}\in {B}\to \left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
82 40 81 ralrimi ${⊢}\left(\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\wedge \left({y}\in {w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\right)\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
83 82 exp32 ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left({y}\in {w}\to \left(\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
84 31 83 reximdai ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
85 84 adantrr ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
86 ssrexv ${⊢}{w}\subseteq {B}\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
87 86 ad2antlr ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
88 85 87 syld ${⊢}\left(\left({B}\subseteq ℝ\wedge {w}\subseteq {B}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
89 88 exp43 ${⊢}{B}\subseteq ℝ\to \left({w}\subseteq {B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \left(\forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)\right)\right)$
90 89 3impd ${⊢}{B}\subseteq ℝ\to \left(\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
91 90 3ad2ant3 ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
92 91 adantr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\to \left(\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \left(\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}{u}\le {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
93 26 92 mpdd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\wedge {w}\in \mathrm{Fin}\right)\to \left(\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
94 93 rexlimdva ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {w}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\wedge \forall {y}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
95 6 94 syld ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to {\phi }\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$