Step | Hyp | Ref
| Expression |
1 | | ovres 6698 |
. . . . 5
⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔) = (𝑓𝐷𝑔)) |
2 | 1 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔) = (𝑓𝐷𝑔)) |
3 | | ressprdsds.a |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ 𝑍) |
4 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) |
5 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(dist‘𝑅) =
(dist‘𝑅) |
6 | 4, 5 | ressds 15896 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑍 → (dist‘𝑅) = (dist‘(𝑅 ↾s 𝐴))) |
7 | 3, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (dist‘𝑅) = (dist‘(𝑅 ↾s 𝐴))) |
8 | 7 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥)) = ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥))) |
9 | 8 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥)))) |
10 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥)))) |
11 | 10 | rneqd 5274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) = ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥)))) |
12 | 11 | uneq1d 3728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) ∪ {0}) = (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥))) ∪ {0})) |
13 | 12 | supeq1d 8235 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) ∪ {0}), ℝ*, < ) =
sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
14 | | eqid 2610 |
. . . . . . 7
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) |
15 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) |
16 | | ressprdsds.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑈) |
18 | | ressprdsds.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
20 | | ressprdsds.r |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑋) |
21 | 20 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) |
22 | 21 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) |
23 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘𝑅) |
24 | 4, 23 | ressbasss 15759 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅) |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(𝑅 ↾s 𝐴)) ⊆ (Base‘𝑅)) |
26 | 25 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (Base‘(𝑅 ↾s 𝐴)) ⊆ (Base‘𝑅)) |
27 | | ss2ixp 7807 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐼 (Base‘(𝑅 ↾s 𝐴)) ⊆ (Base‘𝑅) → X𝑥 ∈
𝐼 (Base‘(𝑅 ↾s 𝐴)) ⊆ X𝑥 ∈
𝐼 (Base‘𝑅)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑥 ∈
𝐼 (Base‘(𝑅 ↾s 𝐴)) ⊆ X𝑥 ∈
𝐼 (Base‘𝑅)) |
29 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))) = (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))) |
30 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) = (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) |
31 | | ressprdsds.t |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
32 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ↾s 𝐴) ∈ V |
33 | 32 | rgenw 2908 |
. . . . . . . . . . . . . 14
⊢
∀𝑥 ∈
𝐼 (𝑅 ↾s 𝐴) ∈ V |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅 ↾s 𝐴) ∈ V) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑅
↾s 𝐴)) =
(Base‘(𝑅
↾s 𝐴)) |
36 | 29, 30, 31, 18, 34, 35 | prdsbas3 15964 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) = X𝑥 ∈ 𝐼 (Base‘(𝑅 ↾s 𝐴))) |
37 | 14, 15, 16, 18, 21, 23 | prdsbas3 15964 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) = X𝑥 ∈ 𝐼 (Base‘𝑅)) |
38 | 28, 36, 37 | 3sstr4d 3611 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) ⊆ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
39 | | ressprdsds.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐻) |
40 | | ressprdsds.h |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 = (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐻) = (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
42 | 39, 41 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
43 | | ressprdsds.y |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
45 | 38, 42, 44 | 3sstr4d 3611 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑌)) |
46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 ⊆ (Base‘𝑌)) |
47 | 44 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
48 | 46, 47 | sseqtrd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 ⊆ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
49 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
50 | 48, 49 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
51 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
52 | 48, 51 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
53 | | eqid 2610 |
. . . . . . 7
⊢
(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) |
54 | 14, 15, 17, 19, 22, 50, 52, 5, 53 | prdsdsval2 15967 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘𝑅)(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
55 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑇 ∈ 𝑉) |
56 | 33 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑅 ↾s 𝐴) ∈ V) |
57 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 = (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
58 | 49, 57 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
59 | 51, 57 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
60 | | eqid 2610 |
. . . . . . 7
⊢
(dist‘(𝑅
↾s 𝐴)) =
(dist‘(𝑅
↾s 𝐴)) |
61 | | eqid 2610 |
. . . . . . 7
⊢
(dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) = (dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) |
62 | 29, 30, 55, 19, 56, 58, 59, 60, 61 | prdsdsval2 15967 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅 ↾s 𝐴))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
63 | 13, 54, 62 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))𝑔) = (𝑓(dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))𝑔)) |
64 | | ressprdsds.d |
. . . . . . 7
⊢ 𝐷 = (dist‘𝑌) |
65 | 43 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
66 | 64, 65 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))) |
67 | 66 | oveqdr 6573 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = (𝑓(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))𝑔)) |
68 | | ressprdsds.e |
. . . . . . 7
⊢ 𝐸 = (dist‘𝐻) |
69 | 40 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (dist‘𝐻) = (dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
70 | 68, 69 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → 𝐸 = (dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))) |
71 | 70 | oveqdr 6573 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐸𝑔) = (𝑓(dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))𝑔)) |
72 | 63, 67, 71 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = (𝑓𝐸𝑔)) |
73 | 2, 72 | eqtr2d 2645 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐸𝑔) = (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔)) |
74 | 73 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐸𝑔) = (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔)) |
75 | | mptexg 6389 |
. . . . . 6
⊢ (𝐼 ∈ 𝑊 → (𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) ∈ V) |
76 | 18, 75 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) ∈ V) |
77 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) = (𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) |
78 | 32, 77 | dmmpti 5936 |
. . . . . 6
⊢ dom
(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) = 𝐼 |
79 | 78 | a1i 11 |
. . . . 5
⊢ (𝜑 → dom (𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)) = 𝐼) |
80 | 29, 31, 76, 30, 79, 61 | prdsdsfn 15948 |
. . . 4
⊢ (𝜑 → (dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) Fn ((Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) × (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))))) |
81 | 42 | sqxpeqd 5065 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) × (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))))) |
82 | 70, 81 | fneq12d 5897 |
. . . 4
⊢ (𝜑 → (𝐸 Fn (𝐵 × 𝐵) ↔ (dist‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) Fn ((Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) × (Base‘(𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))))) |
83 | 80, 82 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐸 Fn (𝐵 × 𝐵)) |
84 | | mptexg 6389 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑊 → (𝑥 ∈ 𝐼 ↦ 𝑅) ∈ V) |
85 | 18, 84 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅) ∈ V) |
86 | | dmmptg 5549 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐼 𝑅 ∈ 𝑋 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
87 | 21, 86 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
88 | 14, 16, 85, 15, 87, 53 | prdsdsfn 15948 |
. . . . 5
⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) Fn ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))))) |
89 | 44 | sqxpeqd 5065 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑌) × (Base‘𝑌)) = ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))))) |
90 | 66, 89 | fneq12d 5897 |
. . . . 5
⊢ (𝜑 → (𝐷 Fn ((Base‘𝑌) × (Base‘𝑌)) ↔ (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) Fn ((Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) × (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))))) |
91 | 88, 90 | mpbird 246 |
. . . 4
⊢ (𝜑 → 𝐷 Fn ((Base‘𝑌) × (Base‘𝑌))) |
92 | | xpss12 5148 |
. . . . 5
⊢ ((𝐵 ⊆ (Base‘𝑌) ∧ 𝐵 ⊆ (Base‘𝑌)) → (𝐵 × 𝐵) ⊆ ((Base‘𝑌) × (Base‘𝑌))) |
93 | 45, 45, 92 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐵 × 𝐵) ⊆ ((Base‘𝑌) × (Base‘𝑌))) |
94 | | fnssres 5918 |
. . . 4
⊢ ((𝐷 Fn ((Base‘𝑌) × (Base‘𝑌)) ∧ (𝐵 × 𝐵) ⊆ ((Base‘𝑌) × (Base‘𝑌))) → (𝐷 ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵)) |
95 | 91, 93, 94 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐷 ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵)) |
96 | | eqfnov2 6665 |
. . 3
⊢ ((𝐸 Fn (𝐵 × 𝐵) ∧ (𝐷 ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵)) → (𝐸 = (𝐷 ↾ (𝐵 × 𝐵)) ↔ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐸𝑔) = (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔))) |
97 | 83, 95, 96 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐸 = (𝐷 ↾ (𝐵 × 𝐵)) ↔ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐸𝑔) = (𝑓(𝐷 ↾ (𝐵 × 𝐵))𝑔))) |
98 | 74, 97 | mpbird 246 |
1
⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵))) |