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 e. Fin /\ A =/= (/) /\ B C_ RR ) -> ( A. x e. A E. y e. B A. z e. B ( y <_ z -> ph ) -> E. y e. B A. z e. B ( y <_ z -> A. x e. A ph ) ) )

Proof

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