prdsbnd

Description: The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	prdsbnd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsbnd.b	$⊢ B = {Base}_{Y}$
	prdsbnd.v	$⊢ V = {Base}_{R (x)}$
	prdsbnd.e	$⊢ E = {dist (R (x)) ↾}_{(V \times V)}$
	prdsbnd.d	$⊢ D = dist (Y)$
	prdsbnd.s	$⊢ φ \to S \in W$
	prdsbnd.i	$⊢ φ \to I \in Fin$
	prdsbnd.r	$⊢ φ \to R Fn I$
	prdsbnd.m	$⊢ (φ \land x \in I) \to E \in Bnd (V)$
Assertion	prdsbnd	$⊢ φ \to D \in Bnd (B)$

Proof

Step	Hyp	Ref	Expression
1		prdsbnd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsbnd.b	$⊢ B = {Base}_{Y}$
3		prdsbnd.v	$⊢ V = {Base}_{R (x)}$
4		prdsbnd.e	$⊢ E = {dist (R (x)) ↾}_{(V \times V)}$
5		prdsbnd.d	$⊢ D = dist (Y)$
6		prdsbnd.s	$⊢ φ \to S \in W$
7		prdsbnd.i	$⊢ φ \to I \in Fin$
8		prdsbnd.r	$⊢ φ \to R Fn I$
9		prdsbnd.m	$⊢ (φ \land x \in I) \to E \in Bnd (V)$
10		eqid	$⊢ S ⨉_{𝑠} (x \in I ⟼ R (x)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
11		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
12		eqid	$⊢ dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
13		fvexd	$⊢ (φ \land x \in I) \to R (x) \in V$
14		bndmet	$⊢ E \in Bnd (V) \to E \in Met (V)$
15	9 14	syl	$⊢ (φ \land x \in I) \to E \in Met (V)$
16	10 11 3 4 12 6 7 13 15	prdsmet	$⊢ φ \to dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) \in Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
17		dffn5	$⊢ R Fn I \leftrightarrow R = (x \in I ⟼ R (x))$
18	8 17	sylib	$⊢ φ \to R = (x \in I ⟼ R (x))$
19	18	oveq2d	$⊢ φ \to S ⨉_{𝑠} R = S ⨉_{𝑠} (x \in I ⟼ R (x))$
20	1 19	syl5eq	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R (x))$
21	20	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
22	5 21	syl5eq	$⊢ φ \to D = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
23	20	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
24	2 23	syl5eq	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
25	24	fveq2d	$⊢ φ \to Met (B) = Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
26	16 22 25	3eltr4d	$⊢ φ \to D \in Met (B)$
27		isbnd3	$⊢ E \in Bnd (V) \leftrightarrow (E \in Met (V) \land \exists w \in ℝ E : V \times V ⟶ [0, w])$
28	27	simprbi	$⊢ E \in Bnd (V) \to \exists w \in ℝ E : V \times V ⟶ [0, w]$
29	9 28	syl	$⊢ (φ \land x \in I) \to \exists w \in ℝ E : V \times V ⟶ [0, w]$
30	29	ralrimiva	$⊢ φ \to \forall x \in I \exists w \in ℝ E : V \times V ⟶ [0, w]$
31		oveq2	$⊢ w = k (x) \to [0, w] = [0, k (x)]$
32	31	feq3d	$⊢ w = k (x) \to (E : V \times V ⟶ [0, w] \leftrightarrow E : V \times V ⟶ [0, k (x)])$
33	32	ac6sfi	$⊢ (I \in Fin \land \forall x \in I \exists w \in ℝ E : V \times V ⟶ [0, w]) \to \exists k (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])$
34	7 30 33	syl2anc	$⊢ φ \to \exists k (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])$
35		frn	$⊢ k : I ⟶ ℝ \to ran k \subseteq ℝ$
36	35	adantl	$⊢ (φ \land k : I ⟶ ℝ) \to ran k \subseteq ℝ$
37		0red	$⊢ φ \to 0 \in ℝ$
38	37	snssd	$⊢ φ \to \{0\} \subseteq ℝ$
39	38	adantr	$⊢ (φ \land k : I ⟶ ℝ) \to \{0\} \subseteq ℝ$
40	36 39	unssd	$⊢ (φ \land k : I ⟶ ℝ) \to ran k \cup \{0\} \subseteq ℝ$
41		ffn	$⊢ k : I ⟶ ℝ \to k Fn I$
42		dffn4	$⊢ k Fn I \leftrightarrow k : I \underset{onto}{⟶} ran k$
43	41 42	sylib	$⊢ k : I ⟶ ℝ \to k : I \underset{onto}{⟶} ran k$
44		fofi	$⊢ (I \in Fin \land k : I \underset{onto}{⟶} ran k) \to ran k \in Fin$
45	7 43 44	syl2an	$⊢ (φ \land k : I ⟶ ℝ) \to ran k \in Fin$
46		snfi	$⊢ \{0\} \in Fin$
47		unfi	$⊢ (ran k \in Fin \land \{0\} \in Fin) \to ran k \cup \{0\} \in Fin$
48	45 46 47	sylancl	$⊢ (φ \land k : I ⟶ ℝ) \to ran k \cup \{0\} \in Fin$
49		ssun2	$⊢ \{0\} \subseteq ran k \cup \{0\}$
50		c0ex	$⊢ 0 \in V$
51	50	snid	$⊢ 0 \in \{0\}$
52	49 51	sselii	$⊢ 0 \in (ran k \cup \{0\})$
53		ne0i	$⊢ 0 \in (ran k \cup \{0\}) \to ran k \cup \{0\} \neq \emptyset$
54	52 53	mp1i	$⊢ (φ \land k : I ⟶ ℝ) \to ran k \cup \{0\} \neq \emptyset$
55		ltso	$⊢ < Or ℝ$
56		fisupcl	$⊢ (< Or ℝ \land (ran k \cup \{0\} \in Fin \land ran k \cup \{0\} \neq \emptyset \land ran k \cup \{0\} \subseteq ℝ)) \to sup (ran k \cup \{0\} ℝ <) \in (ran k \cup \{0\})$
57	55 56	mpan	$⊢ (ran k \cup \{0\} \in Fin \land ran k \cup \{0\} \neq \emptyset \land ran k \cup \{0\} \subseteq ℝ) \to sup (ran k \cup \{0\} ℝ <) \in (ran k \cup \{0\})$
58	48 54 40 57	syl3anc	$⊢ (φ \land k : I ⟶ ℝ) \to sup (ran k \cup \{0\} ℝ <) \in (ran k \cup \{0\})$
59	40 58	sseldd	$⊢ (φ \land k : I ⟶ ℝ) \to sup (ran k \cup \{0\} ℝ <) \in ℝ$
60	59	adantrr	$⊢ (φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to sup (ran k \cup \{0\} ℝ <) \in ℝ$
61		metf	$⊢ D \in Met (B) \to D : B \times B ⟶ ℝ$
62		ffn	$⊢ D : B \times B ⟶ ℝ \to D Fn (B \times B)$
63	26 61 62	3syl	$⊢ φ \to D Fn (B \times B)$
64	63	adantr	$⊢ (φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to D Fn (B \times B)$
65	26	ad2antrr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to D \in Met (B)$
66		simprl	$⊢ (φ \land (f \in B \land g \in B)) \to f \in B$
67	66	adantr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to f \in B$
68		simprr	$⊢ (φ \land (f \in B \land g \in B)) \to g \in B$
69	68	adantr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to g \in B$
70		metcl	$⊢ (D \in Met (B) \land f \in B \land g \in B) \to f D g \in ℝ$
71	65 67 69 70	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to f D g \in ℝ$
72		metge0	$⊢ (D \in Met (B) \land f \in B \land g \in B) \to 0 \leq f D g$
73	65 67 69 72	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to 0 \leq f D g$
74	22	oveqdr	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = f dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) g$
75	6	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to S \in W$
76	7	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to I \in Fin$
77		fvexd	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to R (x) \in V$
78	77	ralrimiva	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R (x) \in V$
79	24	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to B = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
80	66 79	eleqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to f \in {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
81	68 79	eleqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to g \in {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
82	10 11 75 76 78 80 81 3 4 12	prdsdsval3	$⊢ (φ \land (f \in B \land g \in B)) \to f dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
83	74 82	eqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
84	83	adantr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
85	15	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to E \in Met (V)$
86	10 11 75 76 78 3 80	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I f (x) \in V$
87	86	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to f (x) \in V$
88	10 11 75 76 78 3 81	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I g (x) \in V$
89	88	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to g (x) \in V$
90		metcl	$⊢ (E \in Met (V) \land f (x) \in V \land g (x) \in V) \to f (x) E g (x) \in ℝ$
91	85 87 89 90	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to f (x) E g (x) \in ℝ$
92	91	ad2ant2r	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to f (x) E g (x) \in ℝ$
93		ffvelrn	$⊢ (k : I ⟶ ℝ \land x \in I) \to k (x) \in ℝ$
94	93	ad2ant2lr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to k (x) \in ℝ$
95	59	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \to sup (ran k \cup \{0\} ℝ <) \in ℝ$
96	95	adantr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to sup (ran k \cup \{0\} ℝ <) \in ℝ$
97		simprr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to E : V \times V ⟶ [0, k (x)]$
98	87	ad2ant2r	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to f (x) \in V$
99	89	ad2ant2r	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to g (x) \in V$
100	97 98 99	fovrnd	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to f (x) E g (x) \in [0, k (x)]$
101		0re	$⊢ 0 \in ℝ$
102		elicc2	$⊢ (0 \in ℝ \land k (x) \in ℝ) \to (f (x) E g (x) \in [0, k (x)] \leftrightarrow (f (x) E g (x) \in ℝ \land 0 \leq f (x) E g (x) \land f (x) E g (x) \leq k (x)))$
103	101 94 102	sylancr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to (f (x) E g (x) \in [0, k (x)] \leftrightarrow (f (x) E g (x) \in ℝ \land 0 \leq f (x) E g (x) \land f (x) E g (x) \leq k (x)))$
104	100 103	mpbid	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to (f (x) E g (x) \in ℝ \land 0 \leq f (x) E g (x) \land f (x) E g (x) \leq k (x))$
105	104	simp3d	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to f (x) E g (x) \leq k (x)$
106	40	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \to ran k \cup \{0\} \subseteq ℝ$
107	106	adantr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to ran k \cup \{0\} \subseteq ℝ$
108	52 53	mp1i	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to ran k \cup \{0\} \neq \emptyset$
109		fimaxre2	$⊢ (ran k \cup \{0\} \subseteq ℝ \land ran k \cup \{0\} \in Fin) \to \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z$
110	40 48 109	syl2anc	$⊢ (φ \land k : I ⟶ ℝ) \to \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z$
111	110	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \to \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z$
112	111	adantr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z$
113		ssun1	$⊢ ran k \subseteq ran k \cup \{0\}$
114	41	ad2antlr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to k Fn I$
115		simprl	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to x \in I$
116		fnfvelrn	$⊢ (k Fn I \land x \in I) \to k (x) \in ran k$
117	114 115 116	syl2anc	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to k (x) \in ran k$
118	113 117	sseldi	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to k (x) \in (ran k \cup \{0\})$
119		suprub	$⊢ ((ran k \cup \{0\} \subseteq ℝ \land ran k \cup \{0\} \neq \emptyset \land \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z) \land k (x) \in (ran k \cup \{0\})) \to k (x) \leq sup (ran k \cup \{0\} ℝ <)$
120	107 108 112 118 119	syl31anc	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to k (x) \leq sup (ran k \cup \{0\} ℝ <)$
121	92 94 96 105 120	letrd	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land (x \in I \land E : V \times V ⟶ [0, k (x)])) \to f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <)$
122	121	expr	$⊢ (((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \land x \in I) \to (E : V \times V ⟶ [0, k (x)] \to f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <))$
123	122	ralimdva	$⊢ ((φ \land (f \in B \land g \in B)) \land k : I ⟶ ℝ) \to (\forall x \in I E : V \times V ⟶ [0, k (x)] \to \forall x \in I f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <))$
124	123	impr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \forall x \in I f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <)$
125		ovex	$⊢ f (x) E g (x) \in V$
126	125	rgenw	$⊢ \forall x \in I f (x) E g (x) \in V$
127		eqid	$⊢ (x \in I ⟼ f (x) E g (x)) = (x \in I ⟼ f (x) E g (x))$
128		breq1	$⊢ w = f (x) E g (x) \to (w \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <))$
129	127 128	ralrnmptw	$⊢ \forall x \in I f (x) E g (x) \in V \to (\forall w \in ran (x \in I ⟼ f (x) E g (x)) w \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow \forall x \in I f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <))$
130	126 129	ax-mp	$⊢ \forall w \in ran (x \in I ⟼ f (x) E g (x)) w \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow \forall x \in I f (x) E g (x) \leq sup (ran k \cup \{0\} ℝ <)$
131	124 130	sylibr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \forall w \in ran (x \in I ⟼ f (x) E g (x)) w \leq sup (ran k \cup \{0\} ℝ <)$
132	40	ad2ant2r	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to ran k \cup \{0\} \subseteq ℝ$
133	52 53	mp1i	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to ran k \cup \{0\} \neq \emptyset$
134	110	ad2ant2r	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z$
135	52	a1i	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to 0 \in (ran k \cup \{0\})$
136		suprub	$⊢ ((ran k \cup \{0\} \subseteq ℝ \land ran k \cup \{0\} \neq \emptyset \land \exists z \in ℝ \forall w \in (ran k \cup \{0\}) w \leq z) \land 0 \in (ran k \cup \{0\})) \to 0 \leq sup (ran k \cup \{0\} ℝ <)$
137	132 133 134 135 136	syl31anc	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to 0 \leq sup (ran k \cup \{0\} ℝ <)$
138		elsni	$⊢ w \in \{0\} \to w = 0$
139	138	breq1d	$⊢ w \in \{0\} \to (w \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow 0 \leq sup (ran k \cup \{0\} ℝ <))$
140	137 139	syl5ibrcom	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to (w \in \{0\} \to w \leq sup (ran k \cup \{0\} ℝ <))$
141	140	ralrimiv	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \forall w \in \{0\} w \leq sup (ran k \cup \{0\} ℝ <)$
142		ralunb	$⊢ \forall w \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) w \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow (\forall w \in ran (x \in I ⟼ f (x) E g (x)) w \leq sup (ran k \cup \{0\} ℝ <) \land \forall w \in \{0\} w \leq sup (ran k \cup \{0\} ℝ <))$
143	131 141 142	sylanbrc	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \forall w \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) w \leq sup (ran k \cup \{0\} ℝ <)$
144	91	fmpttd	$⊢ (φ \land (f \in B \land g \in B)) \to (x \in I ⟼ f (x) E g (x)) : I ⟶ ℝ$
145	144	frnd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \subseteq ℝ$
146		0red	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \in ℝ$
147	146	snssd	$⊢ (φ \land (f \in B \land g \in B)) \to \{0\} \subseteq ℝ$
148	145 147	unssd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ$
149		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
150	148 149	sstrdi	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
151	150	adantr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
152	60	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to sup (ran k \cup \{0\} ℝ <) \in ℝ$
153	152	rexrd	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to sup (ran k \cup \{0\} ℝ <) \in ℝ^{*}$
154		supxrleub	$⊢ (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{} \land sup (ran k \cup \{0\} ℝ <) \in ℝ^{}) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow \forall w \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) w \leq sup (ran k \cup \{0\} ℝ <))$
155	151 153 154	syl2anc	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq sup (ran k \cup \{0\} ℝ <) \leftrightarrow \forall w \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) w \leq sup (ran k \cup \{0\} ℝ <))$
156	143 155	mpbird	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq sup (ran k \cup \{0\} ℝ <)$
157	84 156	eqbrtrd	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to f D g \leq sup (ran k \cup \{0\} ℝ <)$
158		elicc2	$⊢ (0 \in ℝ \land sup (ran k \cup \{0\} ℝ <) \in ℝ) \to (f D g \in [0, sup (ran k \cup \{0\} ℝ <)] \leftrightarrow (f D g \in ℝ \land 0 \leq f D g \land f D g \leq sup (ran k \cup \{0\} ℝ <)))$
159	101 152 158	sylancr	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to (f D g \in [0, sup (ran k \cup \{0\} ℝ <)] \leftrightarrow (f D g \in ℝ \land 0 \leq f D g \land f D g \leq sup (ran k \cup \{0\} ℝ <)))$
160	71 73 157 159	mpbir3and	$⊢ ((φ \land (f \in B \land g \in B)) \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to f D g \in [0, sup (ran k \cup \{0\} ℝ <)]$
161	160	an32s	$⊢ ((φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \land (f \in B \land g \in B)) \to f D g \in [0, sup (ran k \cup \{0\} ℝ <)]$
162	161	ralrimivva	$⊢ (φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \forall f \in B \forall g \in B f D g \in [0, sup (ran k \cup \{0\} ℝ <)]$
163		ffnov	$⊢ D : B \times B ⟶ [0, sup (ran k \cup \{0\} ℝ <)] \leftrightarrow (D Fn (B \times B) \land \forall f \in B \forall g \in B f D g \in [0, sup (ran k \cup \{0\} ℝ <)])$
164	64 162 163	sylanbrc	$⊢ (φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to D : B \times B ⟶ [0, sup (ran k \cup \{0\} ℝ <)]$
165		oveq2	$⊢ m = sup (ran k \cup \{0\} ℝ <) \to [0, m] = [0, sup (ran k \cup \{0\} ℝ <)]$
166	165	feq3d	$⊢ m = sup (ran k \cup \{0\} ℝ <) \to (D : B \times B ⟶ [0, m] \leftrightarrow D : B \times B ⟶ [0, sup (ran k \cup \{0\} ℝ <)])$
167	166	rspcev	$⊢ (sup (ran k \cup \{0\} ℝ <) \in ℝ \land D : B \times B ⟶ [0, sup (ran k \cup \{0\} ℝ <)]) \to \exists m \in ℝ D : B \times B ⟶ [0, m]$
168	60 164 167	syl2anc	$⊢ (φ \land (k : I ⟶ ℝ \land \forall x \in I E : V \times V ⟶ [0, k (x)])) \to \exists m \in ℝ D : B \times B ⟶ [0, m]$
169	34 168	exlimddv	$⊢ φ \to \exists m \in ℝ D : B \times B ⟶ [0, m]$
170		isbnd3	$⊢ D \in Bnd (B) \leftrightarrow (D \in Met (B) \land \exists m \in ℝ D : B \times B ⟶ [0, m])$
171	26 169 170	sylanbrc	$⊢ φ \to D \in Bnd (B)$

Metamath Proof Explorer

Theorem prdsbnd

Proof