Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
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 ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
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 ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
11 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
12 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
13 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
14 bndmet ⊢ ( 𝐸 ∈ ( Bnd ‘ 𝑉 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
15 9 14 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
16 10 11 3 4 12 6 7 13 15 prdsmet ⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
17 dffn5 ⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
18 8 17 sylib ⊢ ( 𝜑 → 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
19 18 oveq2d ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
20 1 19 eqtrid ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
22 5 21 eqtrid ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
23 20 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
24 2 23 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝐵 ) = ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
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 ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) 𝑔 ) )
75 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑊 )
76 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ Fin )
77 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
78 77 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑅 ‘ 𝑥 ) ∈ V )
79 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
80 66 79 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
81 68 79 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
82 10 11 75 76 78 80 81 3 4 12 prdsdsval3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) 𝑔 ) = 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 ffvelcdm ⊢ ( ( 𝑘 : 𝐼 ⟶ ℝ ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑥 ) ∈ ℝ )
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 fovcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑘 : 𝐼 ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( 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 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑘 : 𝐼 ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( 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 ‘ 𝐵 ) )