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 
|- ( ph -> A e. Fin )
ssfiunibd.b 
|- ( ( ph /\ z e. U. A ) -> B e. RR )
ssfiunibd.bd 
|- ( ( ph /\ x e. A ) -> E. y e. RR A. z e. x B <_ y )
ssfiunibd.ssun 
|- ( ph -> C C_ U. A )
Assertion ssfiunibd 
|- ( ph -> E. w e. RR A. z e. C B <_ w )

Proof

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