Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prdsbnd Structured version   Visualization version   GIF version

Theorem prdsbnd 32762
 Description: The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015.)
Hypotheses
Ref Expression
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
Ref Expression
prdsbnd (𝜑𝐷 ∈ (Bnd‘𝐵))
Distinct variable groups:   𝑥,𝑅   𝑥,𝐵   𝜑,𝑥   𝑥,𝐼   𝑥,𝑆   𝑥,𝑌
Allowed substitution hints:   𝐷(𝑥)   𝐸(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem prdsbnd
Dummy variables 𝑧 𝑓 𝑔 𝑘 𝑚 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2610 . . . 4 (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
2 eqid 2610 . . . 4 (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
3 prdsbnd.v . . . 4 𝑉 = (Base‘(𝑅𝑥))
4 prdsbnd.e . . . 4 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
5 eqid 2610 . . . 4 (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
6 prdsbnd.s . . . 4 (𝜑𝑆𝑊)
7 prdsbnd.i . . . 4 (𝜑𝐼 ∈ Fin)
8 fvex 6113 . . . . 5 (𝑅𝑥) ∈ V
98a1i 11 . . . 4 ((𝜑𝑥𝐼) → (𝑅𝑥) ∈ V)
10 prdsbnd.m . . . . 5 ((𝜑𝑥𝐼) → 𝐸 ∈ (Bnd‘𝑉))
11 bndmet 32750 . . . . 5 (𝐸 ∈ (Bnd‘𝑉) → 𝐸 ∈ (Met‘𝑉))
1210, 11syl 17 . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
131, 2, 3, 4, 5, 6, 7, 9, 12prdsmet 21985 . . 3 (𝜑 → (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
14 prdsbnd.d . . . 4 𝐷 = (dist‘𝑌)
15 prdsbnd.y . . . . . 6 𝑌 = (𝑆Xs𝑅)
16 prdsbnd.r . . . . . . . 8 (𝜑𝑅 Fn 𝐼)
17 dffn5 6151 . . . . . . . 8 (𝑅 Fn 𝐼𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1816, 17sylib 207 . . . . . . 7 (𝜑𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1918oveq2d 6565 . . . . . 6 (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2015, 19syl5eq 2656 . . . . 5 (𝜑𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2120fveq2d 6107 . . . 4 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2214, 21syl5eq 2656 . . 3 (𝜑𝐷 = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
23 prdsbnd.b . . . . 5 𝐵 = (Base‘𝑌)
2420fveq2d 6107 . . . . 5 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2523, 24syl5eq 2656 . . . 4 (𝜑𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2625fveq2d 6107 . . 3 (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
2713, 22, 263eltr4d 2703 . 2 (𝜑𝐷 ∈ (Met‘𝐵))
28 isbnd3 32753 . . . . . . 7 (𝐸 ∈ (Bnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)))
2928simprbi 479 . . . . . 6 (𝐸 ∈ (Bnd‘𝑉) → ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤))
3010, 29syl 17 . . . . 5 ((𝜑𝑥𝐼) → ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤))
3130ralrimiva 2949 . . . 4 (𝜑 → ∀𝑥𝐼𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤))
32 oveq2 6557 . . . . . 6 (𝑤 = (𝑘𝑥) → (0[,]𝑤) = (0[,](𝑘𝑥)))
3332feq3d 5945 . . . . 5 (𝑤 = (𝑘𝑥) → (𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤) ↔ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥))))
3433ac6sfi 8089 . . . 4 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)) → ∃𝑘(𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥))))
357, 31, 34syl2anc 691 . . 3 (𝜑 → ∃𝑘(𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥))))
36 frn 5966 . . . . . . . 8 (𝑘:𝐼⟶ℝ → ran 𝑘 ⊆ ℝ)
3736adantl 481 . . . . . . 7 ((𝜑𝑘:𝐼⟶ℝ) → ran 𝑘 ⊆ ℝ)
38 0red 9920 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
3938snssd 4281 . . . . . . . 8 (𝜑 → {0} ⊆ ℝ)
4039adantr 480 . . . . . . 7 ((𝜑𝑘:𝐼⟶ℝ) → {0} ⊆ ℝ)
4137, 40unssd 3751 . . . . . 6 ((𝜑𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ⊆ ℝ)
42 ffn 5958 . . . . . . . . . 10 (𝑘:𝐼⟶ℝ → 𝑘 Fn 𝐼)
43 dffn4 6034 . . . . . . . . . 10 (𝑘 Fn 𝐼𝑘:𝐼onto→ran 𝑘)
4442, 43sylib 207 . . . . . . . . 9 (𝑘:𝐼⟶ℝ → 𝑘:𝐼onto→ran 𝑘)
45 fofi 8135 . . . . . . . . 9 ((𝐼 ∈ Fin ∧ 𝑘:𝐼onto→ran 𝑘) → ran 𝑘 ∈ Fin)
467, 44, 45syl2an 493 . . . . . . . 8 ((𝜑𝑘:𝐼⟶ℝ) → ran 𝑘 ∈ Fin)
47 snfi 7923 . . . . . . . 8 {0} ∈ Fin
48 unfi 8112 . . . . . . . 8 ((ran 𝑘 ∈ Fin ∧ {0} ∈ Fin) → (ran 𝑘 ∪ {0}) ∈ Fin)
4946, 47, 48sylancl 693 . . . . . . 7 ((𝜑𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ∈ Fin)
50 ssun2 3739 . . . . . . . . 9 {0} ⊆ (ran 𝑘 ∪ {0})
51 c0ex 9913 . . . . . . . . . 10 0 ∈ V
5251snid 4155 . . . . . . . . 9 0 ∈ {0}
5350, 52sselii 3565 . . . . . . . 8 0 ∈ (ran 𝑘 ∪ {0})
54 ne0i 3880 . . . . . . . 8 (0 ∈ (ran 𝑘 ∪ {0}) → (ran 𝑘 ∪ {0}) ≠ ∅)
5553, 54mp1i 13 . . . . . . 7 ((𝜑𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ≠ ∅)
56 ltso 9997 . . . . . . . 8 < Or ℝ
57 fisupcl 8258 . . . . . . . 8 (( < Or ℝ ∧ ((ran 𝑘 ∪ {0}) ∈ Fin ∧ (ran 𝑘 ∪ {0}) ≠ ∅ ∧ (ran 𝑘 ∪ {0}) ⊆ ℝ)) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ (ran 𝑘 ∪ {0}))
5856, 57mpan 702 . . . . . . 7 (((ran 𝑘 ∪ {0}) ∈ Fin ∧ (ran 𝑘 ∪ {0}) ≠ ∅ ∧ (ran 𝑘 ∪ {0}) ⊆ ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ (ran 𝑘 ∪ {0}))
5949, 55, 41, 58syl3anc 1318 . . . . . 6 ((𝜑𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ (ran 𝑘 ∪ {0}))
6041, 59sseldd 3569 . . . . 5 ((𝜑𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
6160adantrr 749 . . . 4 ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
62 metf 21945 . . . . . . 7 (𝐷 ∈ (Met‘𝐵) → 𝐷:(𝐵 × 𝐵)⟶ℝ)
63 ffn 5958 . . . . . . 7 (𝐷:(𝐵 × 𝐵)⟶ℝ → 𝐷 Fn (𝐵 × 𝐵))
6427, 62, 633syl 18 . . . . . 6 (𝜑𝐷 Fn (𝐵 × 𝐵))
6564adantr 480 . . . . 5 ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝐷 Fn (𝐵 × 𝐵))
6627ad2antrr 758 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝐷 ∈ (Met‘𝐵))
67 simprl 790 . . . . . . . . . 10 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
6867adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝑓𝐵)
69 simprr 792 . . . . . . . . . 10 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
7069adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝑔𝐵)
71 metcl 21947 . . . . . . . . 9 ((𝐷 ∈ (Met‘𝐵) ∧ 𝑓𝐵𝑔𝐵) → (𝑓𝐷𝑔) ∈ ℝ)
7266, 68, 70, 71syl3anc 1318 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑓𝐷𝑔) ∈ ℝ)
73 metge0 21960 . . . . . . . . 9 ((𝐷 ∈ (Met‘𝐵) ∧ 𝑓𝐵𝑔𝐵) → 0 ≤ (𝑓𝐷𝑔))
7466, 68, 70, 73syl3anc 1318 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 0 ≤ (𝑓𝐷𝑔))
7522oveqdr 6573 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = (𝑓(dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))𝑔))
766adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
777adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼 ∈ Fin)
788a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑅𝑥) ∈ V)
7978ralrimiva 2949 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑅𝑥) ∈ V)
8025adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
8167, 80eleqtrd 2690 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 ∈ (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
8269, 80eleqtrd 2690 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 ∈ (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
831, 2, 76, 77, 79, 81, 82, 3, 4, 5prdsdsval3 15968 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓(dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
8475, 83eqtrd 2644 . . . . . . . . . 10 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
8584adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
8612adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
871, 2, 76, 77, 79, 3, 81prdsbascl 15966 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8887r19.21bi 2916 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
891, 2, 76, 77, 79, 3, 82prdsbascl 15966 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
9089r19.21bi 2916 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
91 metcl 21947 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
9286, 88, 90, 91syl3anc 1318 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
9392ad2ant2r 779 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
94 ffvelrn 6265 . . . . . . . . . . . . . . . . 17 ((𝑘:𝐼⟶ℝ ∧ 𝑥𝐼) → (𝑘𝑥) ∈ ℝ)
9594ad2ant2lr 780 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑘𝑥) ∈ ℝ)
9660adantlr 747 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
9796adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
98 simprr 792 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))
9988ad2ant2r 779 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑓𝑥) ∈ 𝑉)
10090ad2ant2r 779 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑔𝑥) ∈ 𝑉)
10198, 99, 100fovrnd 6704 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ (0[,](𝑘𝑥)))
102 0re 9919 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
103 elicc2 12109 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ ∧ (𝑘𝑥) ∈ ℝ) → (((𝑓𝑥)𝐸(𝑔𝑥)) ∈ (0[,](𝑘𝑥)) ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (𝑘𝑥))))
104102, 95, 103sylancr 694 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (((𝑓𝑥)𝐸(𝑔𝑥)) ∈ (0[,](𝑘𝑥)) ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (𝑘𝑥))))
105101, 104mpbid 221 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (𝑘𝑥)))
106105simp3d 1068 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (𝑘𝑥))
10741adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ⊆ ℝ)
108107adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (ran 𝑘 ∪ {0}) ⊆ ℝ)
10953, 54mp1i 13 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (ran 𝑘 ∪ {0}) ≠ ∅)
110 fimaxre2 10848 . . . . . . . . . . . . . . . . . . . 20 (((ran 𝑘 ∪ {0}) ⊆ ℝ ∧ (ran 𝑘 ∪ {0}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧)
11141, 49, 110syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘:𝐼⟶ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧)
112111adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧)
113112adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧)
114 ssun1 3738 . . . . . . . . . . . . . . . . . 18 ran 𝑘 ⊆ (ran 𝑘 ∪ {0})
11542ad2antlr 759 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝑘 Fn 𝐼)
116 simprl 790 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝑥𝐼)
117 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . 19 ((𝑘 Fn 𝐼𝑥𝐼) → (𝑘𝑥) ∈ ran 𝑘)
118115, 116, 117syl2anc 691 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑘𝑥) ∈ ran 𝑘)
119114, 118sseldi 3566 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑘𝑥) ∈ (ran 𝑘 ∪ {0}))
120 suprub 10863 . . . . . . . . . . . . . . . . 17 ((((ran 𝑘 ∪ {0}) ⊆ ℝ ∧ (ran 𝑘 ∪ {0}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧) ∧ (𝑘𝑥) ∈ (ran 𝑘 ∪ {0})) → (𝑘𝑥) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
121108, 109, 113, 119, 120syl31anc 1321 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑘𝑥) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
12293, 95, 97, 106, 121letrd 10073 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥𝐼𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
123122expr 641 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ 𝑥𝐼) → (𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
124123ralimdva 2945 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑘:𝐼⟶ℝ) → (∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
125124impr 647 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
126 ovex 6577 . . . . . . . . . . . . . 14 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
127126rgenw 2908 . . . . . . . . . . . . 13 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
128 eqid 2610 . . . . . . . . . . . . . 14 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
129 breq1 4586 . . . . . . . . . . . . . 14 (𝑤 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
130128, 129ralrnmpt 6276 . . . . . . . . . . . . 13 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑤 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
131127, 130ax-mp 5 . . . . . . . . . . . 12 (∀𝑤 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
132125, 131sylibr 223 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∀𝑤 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
13341ad2ant2r 779 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (ran 𝑘 ∪ {0}) ⊆ ℝ)
13453, 54mp1i 13 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (ran 𝑘 ∪ {0}) ≠ ∅)
135111ad2ant2r 779 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧)
13653a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 0 ∈ (ran 𝑘 ∪ {0}))
137 suprub 10863 . . . . . . . . . . . . . 14 ((((ran 𝑘 ∪ {0}) ⊆ ℝ ∧ (ran 𝑘 ∪ {0}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤𝑧) ∧ 0 ∈ (ran 𝑘 ∪ {0})) → 0 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
138133, 134, 135, 136, 137syl31anc 1321 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 0 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
139 elsni 4142 . . . . . . . . . . . . . 14 (𝑤 ∈ {0} → 𝑤 = 0)
140139breq1d 4593 . . . . . . . . . . . . 13 (𝑤 ∈ {0} → (𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ 0 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
141138, 140syl5ibrcom 236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑤 ∈ {0} → 𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
142141ralrimiv 2948 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∀𝑤 ∈ {0}𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
143 ralunb 3756 . . . . . . . . . . 11 (∀𝑤 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ (∀𝑤 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ∧ ∀𝑤 ∈ {0}𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
144132, 142, 143sylanbrc 695 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∀𝑤 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
14592, 128fmptd 6292 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ)
146 frn 5966 . . . . . . . . . . . . . . 15 ((𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ)
147145, 146syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ)
148 0red 9920 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ)
149148snssd 4281 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ)
150147, 149unssd 3751 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ)
151 ressxr 9962 . . . . . . . . . . . . 13 ℝ ⊆ ℝ*
152150, 151syl6ss 3580 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
153152adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
15461adantlr 747 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
155154rexrd 9968 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ*)
156 supxrleub 12028 . . . . . . . . . . 11 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ∀𝑤 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
157153, 155, 156syl2anc 691 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ∀𝑤 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )))
158144, 157mpbird 246 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
15985, 158eqbrtrd 4605 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))
160 elicc2 12109 . . . . . . . . 9 ((0 ∈ ℝ ∧ sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ) → ((𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ ((𝑓𝐷𝑔) ∈ ℝ ∧ 0 ≤ (𝑓𝐷𝑔) ∧ (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))))
161102, 154, 160sylancr 694 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ((𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ ((𝑓𝐷𝑔) ∈ ℝ ∧ 0 ≤ (𝑓𝐷𝑔) ∧ (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ))))
16272, 74, 159, 161mpbir3and 1238 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )))
163162an32s 842 . . . . . 6 (((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )))
164163ralrimivva 2954 . . . . 5 ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∀𝑓𝐵𝑔𝐵 (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )))
165 ffnov 6662 . . . . 5 (𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ (𝐷 Fn (𝐵 × 𝐵) ∧ ∀𝑓𝐵𝑔𝐵 (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < ))))
16665, 164, 165sylanbrc 695 . . . 4 ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )))
167 oveq2 6557 . . . . . 6 (𝑚 = sup((ran 𝑘 ∪ {0}), ℝ, < ) → (0[,]𝑚) = (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )))
168167feq3d 5945 . . . . 5 (𝑚 = sup((ran 𝑘 ∪ {0}), ℝ, < ) → (𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚) ↔ 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < ))))
169168rspcev 3282 . . . 4 ((sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ ∧ 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < ))) → ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚))
17061, 166, 169syl2anc 691 . . 3 ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘𝑥)))) → ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚))
17135, 170exlimddv 1850 . 2 (𝜑 → ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚))
172 isbnd3 32753 . 2 (𝐷 ∈ (Bnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚)))
17327, 171, 172sylanbrc 695 1 (𝜑𝐷 ∈ (Bnd‘𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   Or wor 4958   × cxp 5036  ran crn 5039   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℝcr 9814  0cc0 9815  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  [,]cicc 12049  Basecbs 15695  distcds 15777  Xscprds 15929  Metcme 19553  Bndcbnd 32736 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-ec 7631  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-icc 12053  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-hom 15793  df-cco 15794  df-prds 15931  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-bnd 32748 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator