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 
|- Y = ( S Xs_ R )
prdsbnd.b 
|- B = ( Base ` Y )
prdsbnd.v 
|- V = ( Base ` ( R ` x ) )
prdsbnd.e 
|- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
prdsbnd.d 
|- D = ( dist ` Y )
prdsbnd.s 
|- ( ph -> S e. W )
prdsbnd.i 
|- ( ph -> I e. Fin )
prdsbnd.r 
|- ( ph -> R Fn I )
prdsbnd.m 
|- ( ( ph /\ x e. I ) -> E e. ( Bnd ` V ) )
Assertion prdsbnd 
|- ( ph -> D e. ( Bnd ` B ) )

Proof

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