ssfiunibd

Description: A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ssfiunibd.fi	$⊢ φ \to A \in Fin$
	ssfiunibd.b	$⊢ (φ \land z \in ⋃ A) \to B \in ℝ$
	ssfiunibd.bd	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall z \in x B \leq y$
	ssfiunibd.ssun	$⊢ φ \to C \subseteq ⋃ A$
Assertion	ssfiunibd	$⊢ φ \to \exists w \in ℝ \forall z \in C B \leq w$

Proof

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

Metamath Proof Explorer

Theorem ssfiunibd

Proof