# 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 $⊢ φ → A ∈ Fin$
ssfiunibd.b $⊢ φ ∧ z ∈ ⋃ A → B ∈ ℝ$
ssfiunibd.bd $⊢ φ ∧ x ∈ A → ∃ y ∈ ℝ ∀ z ∈ x B ≤ y$
ssfiunibd.ssun $⊢ φ → C ⊆ ⋃ A$
Assertion ssfiunibd $⊢ φ → ∃ w ∈ ℝ ∀ z ∈ C B ≤ w$

### Proof

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