Metamath Proof Explorer

Theorem filbcmb

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

Ref Expression
Assertion filbcmb ⊢A∈Fin∧A≠∅∧B⊆ℝ→∀x∈A∃y∈B∀z∈By≤z→φ→∃y∈B∀z∈By≤z→∀x∈Aφ

Proof

Step Hyp Ref Expression
1 reex ⊢ℝ∈V
2 1 ssex ⊢B⊆ℝ→B∈V
3 indexfi ⊢A∈Fin∧B∈V∧∀x∈A∃y∈B∀z∈By≤z→φ→∃w∈Finw⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ
4 3 3expia ⊢A∈Fin∧B∈V→∀x∈A∃y∈B∀z∈By≤z→φ→∃w∈Finw⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ
5 2 4 sylan2 ⊢A∈Fin∧B⊆ℝ→∀x∈A∃y∈B∀z∈By≤z→φ→∃w∈Finw⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ
6 5 3adant2 ⊢A∈Fin∧A≠∅∧B⊆ℝ→∀x∈A∃y∈B∀z∈By≤z→φ→∃w∈Finw⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ
7 r19.2z ⊢A≠∅∧∀x∈A∃y∈w∀z∈By≤z→φ→∃x∈A∃y∈w∀z∈By≤z→φ
8 rexn0 ⊢∃y∈w∀z∈By≤z→φ→w≠∅
9 8 rexlimivw ⊢∃x∈A∃y∈w∀z∈By≤z→φ→w≠∅
10 7 9 syl ⊢A≠∅∧∀x∈A∃y∈w∀z∈By≤z→φ→w≠∅
11 10 ex ⊢A≠∅→∀x∈A∃y∈w∀z∈By≤z→φ→w≠∅
12 11 3ad2ant2 ⊢A∈Fin∧A≠∅∧B⊆ℝ→∀x∈A∃y∈w∀z∈By≤z→φ→w≠∅
13 12 ad2antrr ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin∧w⊆B→∀x∈A∃y∈w∀z∈By≤z→φ→w≠∅
14 sstr ⊢w⊆B∧B⊆ℝ→w⊆ℝ
15 14 ancoms ⊢B⊆ℝ∧w⊆B→w⊆ℝ
16 fimaxre ⊢w⊆ℝ∧w∈Fin∧w≠∅→∃y∈w∀u∈wu≤y
17 16 3expia ⊢w⊆ℝ∧w∈Fin→w≠∅→∃y∈w∀u∈wu≤y
18 15 17 sylan ⊢B⊆ℝ∧w⊆B∧w∈Fin→w≠∅→∃y∈w∀u∈wu≤y
19 18 anasss ⊢B⊆ℝ∧w⊆B∧w∈Fin→w≠∅→∃y∈w∀u∈wu≤y
20 19 ancom2s ⊢B⊆ℝ∧w∈Fin∧w⊆B→w≠∅→∃y∈w∀u∈wu≤y
21 20 3ad2antl3 ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin∧w⊆B→w≠∅→∃y∈w∀u∈wu≤y
22 21 anassrs ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin∧w⊆B→w≠∅→∃y∈w∀u∈wu≤y
23 13 22 syld ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin∧w⊆B→∀x∈A∃y∈w∀z∈By≤z→φ→∃y∈w∀u∈wu≤y
24 23 a1dd ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin∧w⊆B→∀x∈A∃y∈w∀z∈By≤z→φ→∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y
25 24 ex ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin→w⊆B→∀x∈A∃y∈w∀z∈By≤z→φ→∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y
26 25 3impd ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin→w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y
27 nfv ⊢ℲyB⊆ℝ∧w⊆B
28 nfcv ⊢Ⅎ_yA
29 nfre1 ⊢Ⅎy∃y∈w∀z∈By≤z→φ
30 28 29 nfralw ⊢Ⅎy∀x∈A∃y∈w∀z∈By≤z→φ
31 27 30 nfan ⊢ℲyB⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ
32 nfv ⊢ℲzB⊆ℝ∧w⊆B
33 nfcv ⊢Ⅎ_zA
34 nfcv ⊢Ⅎ_zw
35 nfra1 ⊢Ⅎz∀z∈By≤z→φ
36 34 35 nfrexw ⊢Ⅎz∃y∈w∀z∈By≤z→φ
37 33 36 nfralw ⊢Ⅎz∀x∈A∃y∈w∀z∈By≤z→φ
38 32 37 nfan ⊢ℲzB⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ
39 nfv ⊢Ⅎzy∈w∧∀u∈wu≤y
40 38 39 nfan ⊢ℲzB⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧y∈w∧∀u∈wu≤y
41 breq1 ⊢y=v→y≤z↔v≤z
42 41 imbi1d ⊢y=v→y≤z→φ↔v≤z→φ
43 42 ralbidv ⊢y=v→∀z∈By≤z→φ↔∀z∈Bv≤z→φ
44 43 cbvrexvw ⊢∃y∈w∀z∈By≤z→φ↔∃v∈w∀z∈Bv≤z→φ
45 rsp ⊢∀z∈Bv≤z→φ→z∈B→v≤z→φ
46 ssel2 ⊢w⊆B∧v∈w→v∈B
47 ssel2 ⊢B⊆ℝ∧v∈B→v∈ℝ
48 46 47 sylan2 ⊢B⊆ℝ∧w⊆B∧v∈w→v∈ℝ
49 48 anassrs ⊢B⊆ℝ∧w⊆B∧v∈w→v∈ℝ
50 49 adantlr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧v∈w→v∈ℝ
51 50 adantlr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→v∈ℝ
52 ssel2 ⊢w⊆B∧y∈w→y∈B
53 ssel2 ⊢B⊆ℝ∧y∈B→y∈ℝ
54 52 53 sylan2 ⊢B⊆ℝ∧w⊆B∧y∈w→y∈ℝ
55 54 anassrs ⊢B⊆ℝ∧w⊆B∧y∈w→y∈ℝ
56 55 adantrr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y→y∈ℝ
57 56 ad2antrr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→y∈ℝ
58 ssel2 ⊢B⊆ℝ∧z∈B→z∈ℝ
59 58 adantlr ⊢B⊆ℝ∧w⊆B∧z∈B→z∈ℝ
60 59 ad2ant2r ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z→z∈ℝ
61 60 adantr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→z∈ℝ
62 breq1 ⊢u=v→u≤y↔v≤y
63 62 rspccva ⊢∀u∈wu≤y∧v∈w→v≤y
64 63 adantll ⊢y∈w∧∀u∈wu≤y∧v∈w→v≤y
65 64 adantll ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧v∈w→v≤y
66 65 adantlr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→v≤y
67 simplrr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→y≤z
68 51 57 61 66 67 letrd ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→v≤z
69 pm2.27 ⊢z∈B→z∈B→v≤z→φ→v≤z→φ
70 69 adantr ⊢z∈B∧y≤z→z∈B→v≤z→φ→v≤z→φ
71 70 ad2antlr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→z∈B→v≤z→φ→v≤z→φ
72 68 71 mpid ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→z∈B→v≤z→φ→φ
73 45 72 syl5 ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧v∈w→∀z∈Bv≤z→φ→φ
74 73 adantlr ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧x∈A∧v∈w→∀z∈Bv≤z→φ→φ
75 74 rexlimdva ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧x∈A→∃v∈w∀z∈Bv≤z→φ→φ
76 44 75 biimtrid ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧x∈A→∃y∈w∀z∈By≤z→φ→φ
77 76 ralimdva ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z→∀x∈A∃y∈w∀z∈By≤z→φ→∀x∈Aφ
78 77 imp ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧z∈B∧y≤z∧∀x∈A∃y∈w∀z∈By≤z→φ→∀x∈Aφ
79 78 an32s ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧∀x∈A∃y∈w∀z∈By≤z→φ∧z∈B∧y≤z→∀x∈Aφ
80 79 exp32 ⊢B⊆ℝ∧w⊆B∧y∈w∧∀u∈wu≤y∧∀x∈A∃y∈w∀z∈By≤z→φ→z∈B→y≤z→∀x∈Aφ
81 80 an32s ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧y∈w∧∀u∈wu≤y→z∈B→y≤z→∀x∈Aφ
82 40 81 ralrimi ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧y∈w∧∀u∈wu≤y→∀z∈By≤z→∀x∈Aφ
83 82 exp32 ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ→y∈w→∀u∈wu≤y→∀z∈By≤z→∀x∈Aφ
84 31 83 reximdai ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈w∀z∈By≤z→∀x∈Aφ
85 84 adantrr ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈w∀z∈By≤z→∀x∈Aφ
86 ssrexv ⊢w⊆B→∃y∈w∀z∈By≤z→∀x∈Aφ→∃y∈B∀z∈By≤z→∀x∈Aφ
87 86 ad2antlr ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀z∈By≤z→∀x∈Aφ→∃y∈B∀z∈By≤z→∀x∈Aφ
88 85 87 syld ⊢B⊆ℝ∧w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈B∀z∈By≤z→∀x∈Aφ
89 88 exp43 ⊢B⊆ℝ→w⊆B→∀x∈A∃y∈w∀z∈By≤z→φ→∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈B∀z∈By≤z→∀x∈Aφ
90 89 3impd ⊢B⊆ℝ→w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈B∀z∈By≤z→∀x∈Aφ
91 90 3ad2ant3 ⊢A∈Fin∧A≠∅∧B⊆ℝ→w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈B∀z∈By≤z→∀x∈Aφ
92 91 adantr ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin→w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈w∀u∈wu≤y→∃y∈B∀z∈By≤z→∀x∈Aφ
93 26 92 mpdd ⊢A∈Fin∧A≠∅∧B⊆ℝ∧w∈Fin→w⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈B∀z∈By≤z→∀x∈Aφ
94 93 rexlimdva ⊢A∈Fin∧A≠∅∧B⊆ℝ→∃w∈Finw⊆B∧∀x∈A∃y∈w∀z∈By≤z→φ∧∀y∈w∃x∈A∀z∈By≤z→φ→∃y∈B∀z∈By≤z→∀x∈Aφ
95 6 94 syld ⊢A∈Fin∧A≠∅∧B⊆ℝ→∀x∈A∃y∈B∀z∈By≤z→φ→∃y∈B∀z∈By≤z→∀x∈Aφ