Step | Hyp | Ref
| 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 |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
10 | | prdsbnd.m |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Bnd‘𝑉)) |
11 | | bndmet 32750 |
. . . . 5
⊢ (𝐸 ∈ (Bnd‘𝑉) → 𝐸 ∈ (Met‘𝑉)) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
13 | 1, 2, 3, 4, 5, 6, 7, 9, 12 | prdsmet 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 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
18 | 16, 17 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
19 | 18 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
20 | 15, 19 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
21 | 20 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
22 | 14, 21 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
23 | | prdsbnd.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
24 | 20 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
25 | 23, 24 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
26 | 25 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (Met‘𝐵) =
(Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
27 | 13, 22, 26 | 3eltr4d 2703 |
. 2
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
28 | | isbnd3 32753 |
. . . . . . 7
⊢ (𝐸 ∈ (Bnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤))) |
29 | 28 | simprbi 479 |
. . . . . 6
⊢ (𝐸 ∈ (Bnd‘𝑉) → ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)) |
30 | 10, 29 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)) |
31 | 30 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)) |
32 | | oveq2 6557 |
. . . . . 6
⊢ (𝑤 = (𝑘‘𝑥) → (0[,]𝑤) = (0[,](𝑘‘𝑥))) |
33 | 32 | feq3d 5945 |
. . . . 5
⊢ (𝑤 = (𝑘‘𝑥) → (𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤) ↔ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) |
34 | 33 | ac6sfi 8089 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ ℝ 𝐸:(𝑉 × 𝑉)⟶(0[,]𝑤)) → ∃𝑘(𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) |
35 | 7, 31, 34 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∃𝑘(𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) |
36 | | frn 5966 |
. . . . . . . 8
⊢ (𝑘:𝐼⟶ℝ → ran 𝑘 ⊆
ℝ) |
37 | 36 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → ran 𝑘 ⊆
ℝ) |
38 | | 0red 9920 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
39 | 38 | snssd 4281 |
. . . . . . . 8
⊢ (𝜑 → {0} ⊆
ℝ) |
40 | 39 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → {0} ⊆
ℝ) |
41 | 37, 40 | unssd 3751 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ⊆
ℝ) |
42 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑘:𝐼⟶ℝ → 𝑘 Fn 𝐼) |
43 | | dffn4 6034 |
. . . . . . . . . 10
⊢ (𝑘 Fn 𝐼 ↔ 𝑘:𝐼–onto→ran 𝑘) |
44 | 42, 43 | sylib 207 |
. . . . . . . . 9
⊢ (𝑘:𝐼⟶ℝ → 𝑘:𝐼–onto→ran 𝑘) |
45 | | fofi 8135 |
. . . . . . . . 9
⊢ ((𝐼 ∈ Fin ∧ 𝑘:𝐼–onto→ran 𝑘) → ran 𝑘 ∈ Fin) |
46 | 7, 44, 45 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → ran 𝑘 ∈ Fin) |
47 | | snfi 7923 |
. . . . . . . 8
⊢ {0}
∈ Fin |
48 | | unfi 8112 |
. . . . . . . 8
⊢ ((ran
𝑘 ∈ Fin ∧ {0}
∈ Fin) → (ran 𝑘
∪ {0}) ∈ Fin) |
49 | 46, 47, 48 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ∈
Fin) |
50 | | ssun2 3739 |
. . . . . . . . 9
⊢ {0}
⊆ (ran 𝑘 ∪
{0}) |
51 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
52 | 51 | snid 4155 |
. . . . . . . . 9
⊢ 0 ∈
{0} |
53 | 50, 52 | sselii 3565 |
. . . . . . . 8
⊢ 0 ∈
(ran 𝑘 ∪
{0}) |
54 | | ne0i 3880 |
. . . . . . . 8
⊢ (0 ∈
(ran 𝑘 ∪ {0}) →
(ran 𝑘 ∪ {0}) ≠
∅) |
55 | 53, 54 | mp1i 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})) |
58 | 56, 57 | mpan 702 |
. . . . . . 7
⊢ (((ran
𝑘 ∪ {0}) ∈ Fin
∧ (ran 𝑘 ∪ {0})
≠ ∅ ∧ (ran 𝑘
∪ {0}) ⊆ ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ (ran
𝑘 ∪
{0})) |
59 | 49, 55, 41, 58 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < )
∈ (ran 𝑘 ∪
{0})) |
60 | 41, 59 | sseldd 3569 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < )
∈ ℝ) |
61 | 60 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈
ℝ) |
62 | | metf 21945 |
. . . . . . 7
⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷:(𝐵 × 𝐵)⟶ℝ) |
63 | | ffn 5958 |
. . . . . . 7
⊢ (𝐷:(𝐵 × 𝐵)⟶ℝ → 𝐷 Fn (𝐵 × 𝐵)) |
64 | 27, 62, 63 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) |
65 | 64 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝐷 Fn (𝐵 × 𝐵)) |
66 | 27 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝐷 ∈ (Met‘𝐵)) |
67 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
68 | 67 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝑓 ∈ 𝐵) |
69 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
70 | 69 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝑔 ∈ 𝐵) |
71 | | metcl 21947 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓𝐷𝑔) ∈ ℝ) |
72 | 66, 68, 70, 71 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑓𝐷𝑔) ∈ ℝ) |
73 | | metge0 21960 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 0 ≤ (𝑓𝐷𝑔)) |
74 | 66, 68, 70, 73 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 0 ≤ (𝑓𝐷𝑔)) |
75 | 22 | oveqdr 6573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = (𝑓(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))𝑔)) |
76 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑊) |
77 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ Fin) |
78 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
79 | 78 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V) |
80 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
81 | 67, 80 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
82 | 69, 80 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
83 | 1, 2, 76, 77, 79, 81, 82, 3, 4, 5 | prdsdsval3 15968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
84 | 75, 83 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
85 | 84 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑓𝐷𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
86 | 12 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
87 | 1, 2, 76, 77, 79, 3, 81 | prdsbascl 15966 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉) |
88 | 87 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ 𝑉) |
89 | 1, 2, 76, 77, 79, 3, 82 | prdsbascl 15966 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
90 | 89 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝑉) |
91 | | metcl 21947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ∈ (Met‘𝑉) ∧ (𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
92 | 86, 88, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
93 | 92 | ad2ant2r 779 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
94 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘:𝐼⟶ℝ ∧ 𝑥 ∈ 𝐼) → (𝑘‘𝑥) ∈ ℝ) |
95 | 94 | ad2ant2lr 780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑘‘𝑥) ∈ ℝ) |
96 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) → sup((ran 𝑘 ∪ {0}), ℝ, < )
∈ ℝ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈
ℝ) |
98 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥))) |
99 | 88 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑓‘𝑥) ∈ 𝑉) |
100 | 90 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑔‘𝑥) ∈ 𝑉) |
101 | 98, 99, 100 | fovrnd 6704 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ (0[,](𝑘‘𝑥))) |
102 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
103 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ (𝑘‘𝑥) ∈ ℝ) → (((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ (0[,](𝑘‘𝑥)) ↔ (((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∧ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ (𝑘‘𝑥)))) |
104 | 102, 95, 103 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ (0[,](𝑘‘𝑥)) ↔ (((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∧ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ (𝑘‘𝑥)))) |
105 | 101, 104 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∧ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ (𝑘‘𝑥))) |
106 | 105 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ (𝑘‘𝑥)) |
107 | 41 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) → (ran 𝑘 ∪ {0}) ⊆
ℝ) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (ran 𝑘 ∪ {0}) ⊆ ℝ) |
109 | 53, 54 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (ran 𝑘 ∪ {0}) ≠ ∅) |
110 | | fimaxre2 10848 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ran
𝑘 ∪ {0}) ⊆
ℝ ∧ (ran 𝑘 ∪
{0}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) |
111 | 41, 49, 110 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘:𝐼⟶ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) |
112 | 111 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) |
114 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . 18
⊢ ran 𝑘 ⊆ (ran 𝑘 ∪ {0}) |
115 | 42 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝑘 Fn 𝐼) |
116 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝑥 ∈ 𝐼) |
117 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → (𝑘‘𝑥) ∈ ran 𝑘) |
118 | 115, 116,
117 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑘‘𝑥) ∈ ran 𝑘) |
119 | 114, 118 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑘‘𝑥) ∈ (ran 𝑘 ∪ {0})) |
120 | | suprub 10863 |
. . . . . . . . . . . . . . . . 17
⊢ ((((ran
𝑘 ∪ {0}) ⊆
ℝ ∧ (ran 𝑘 ∪
{0}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) ∧ (𝑘‘𝑥) ∈ (ran 𝑘 ∪ {0})) → (𝑘‘𝑥) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
121 | 108, 109,
113, 119, 120 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑘‘𝑥) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
122 | 93, 95, 97, 106, 121 | letrd 10073 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ (𝑥 ∈ 𝐼 ∧ 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
123 | 122 | expr 641 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) ∧ 𝑥 ∈ 𝐼) → (𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
124 | 123 | ralimdva 2945 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑘:𝐼⟶ℝ) → (∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
125 | 124 | impr 647 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
126 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ V |
127 | 126 | rgenw 2908 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ V |
128 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) |
129 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) → (𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
130 | 128, 129 | ralrnmpt 6276 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ V → (∀𝑤 ∈ ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔
∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
131 | 127, 130 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∀𝑤 ∈
ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔
∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
132 | 125, 131 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∀𝑤 ∈ ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
133 | 41 | ad2ant2r 779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (ran 𝑘 ∪ {0}) ⊆ ℝ) |
134 | 53, 54 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (ran 𝑘 ∪ {0}) ≠ ∅) |
135 | 111 | ad2ant2r 779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) |
136 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 0 ∈ (ran 𝑘 ∪ {0})) |
137 | | suprub 10863 |
. . . . . . . . . . . . . 14
⊢ ((((ran
𝑘 ∪ {0}) ⊆
ℝ ∧ (ran 𝑘 ∪
{0}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (ran 𝑘 ∪ {0})𝑤 ≤ 𝑧) ∧ 0 ∈ (ran 𝑘 ∪ {0})) → 0 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
138 | 133, 134,
135, 136, 137 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 0 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
139 | | elsni 4142 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
140 | 139 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {0} → (𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < )
↔ 0 ≤ sup((ran 𝑘
∪ {0}), ℝ, < ))) |
141 | 138, 140 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑤 ∈ {0} → 𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
142 | 141 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∀𝑤 ∈ {0}𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
143 | | ralunb 3756 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ↔
(∀𝑤 ∈ ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥)))𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, < ) ∧
∀𝑤 ∈ {0}𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
144 | 132, 142,
143 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∀𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
145 | 92, 128 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ) |
146 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
148 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ∈ ℝ) |
149 | 148 | snssd 4281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → {0} ⊆
ℝ) |
150 | 147, 149 | unssd 3751 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ) |
151 | | ressxr 9962 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
152 | 150, 151 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ*) |
153 | 152 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ*) |
154 | 61 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈
ℝ) |
155 | 154 | rexrd 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}), ℝ, <
))) |
157 | 153, 155,
156 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
≤ sup((ran 𝑘 ∪ {0}),
ℝ, < ) ↔ ∀𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})𝑤 ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
158 | 144, 157 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
≤ sup((ran 𝑘 ∪ {0}),
ℝ, < )) |
159 | 85, 158 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)) |
160 | | elicc2 12109 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ sup((ran 𝑘 ∪ {0}), ℝ, < ) ∈ ℝ)
→ ((𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ ((𝑓𝐷𝑔) ∈ ℝ ∧ 0 ≤ (𝑓𝐷𝑔) ∧ (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)))) |
161 | 102, 154,
160 | sylancr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ((𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ ((𝑓𝐷𝑔) ∈ ℝ ∧ 0 ≤ (𝑓𝐷𝑔) ∧ (𝑓𝐷𝑔) ≤ sup((ran 𝑘 ∪ {0}), ℝ, <
)))) |
162 | 72, 74, 159, 161 | mpbir3and 1238 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
163 | 162 | an32s 842 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
164 | 163 | ralrimivva 2954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
165 | | ffnov 6662 |
. . . . 5
⊢ (𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < )) ↔ (𝐷 Fn (𝐵 × 𝐵) ∧ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ (0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
)))) |
166 | 65, 164, 165 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
))) |
167 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = sup((ran 𝑘 ∪ {0}), ℝ, < ) →
(0[,]𝑚) = (0[,]sup((ran
𝑘 ∪ {0}), ℝ, <
))) |
168 | 167 | feq3d 5945 |
. . . . 5
⊢ (𝑚 = sup((ran 𝑘 ∪ {0}), ℝ, < ) → (𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚) ↔ 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, <
)))) |
169 | 168 | rspcev 3282 |
. . . 4
⊢
((sup((ran 𝑘 ∪
{0}), ℝ, < ) ∈ ℝ ∧ 𝐷:(𝐵 × 𝐵)⟶(0[,]sup((ran 𝑘 ∪ {0}), ℝ, < ))) →
∃𝑚 ∈ ℝ
𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚)) |
170 | 61, 166, 169 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ (𝑘:𝐼⟶ℝ ∧ ∀𝑥 ∈ 𝐼 𝐸:(𝑉 × 𝑉)⟶(0[,](𝑘‘𝑥)))) → ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚)) |
171 | 35, 170 | exlimddv 1850 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚)) |
172 | | isbnd3 32753 |
. 2
⊢ (𝐷 ∈ (Bnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∃𝑚 ∈ ℝ 𝐷:(𝐵 × 𝐵)⟶(0[,]𝑚))) |
173 | 27, 171, 172 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐷 ∈ (Bnd‘𝐵)) |