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	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
	prdsbnd.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbnd.v	⊢ 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
	prdsbnd.e	⊢ 𝐸 = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( 𝑉 × 𝑉 ) )
	prdsbnd.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
	prdsbnd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	prdsbnd.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	prdsbnd.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsbnd.m	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Bnd ‘ 𝑉 ) )
Assertion	prdsbnd	⊢ ( 𝜑 → 𝐷 ∈ ( Bnd ‘ 𝐵 ) )

Proof

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

Metamath Proof Explorer

Theorem prdsbnd

Proof