Step | Hyp | Ref
| Expression |
1 | | prdsmet.y |
. . 3
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | prdsmet.b |
. . 3
β’ π΅ = (Baseβπ) |
3 | | prdsmet.v |
. . 3
β’ π = (Baseβπ
) |
4 | | prdsmet.e |
. . 3
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
5 | | prdsmet.d |
. . 3
β’ π· = (distβπ) |
6 | | prdsmet.s |
. . 3
β’ (π β π β π) |
7 | | prdsmet.i |
. . 3
β’ (π β πΌ β Fin) |
8 | | prdsmet.r |
. . 3
β’ ((π β§ π₯ β πΌ) β π
β π) |
9 | | prdsmet.m |
. . . 4
β’ ((π β§ π₯ β πΌ) β πΈ β (Metβπ)) |
10 | | metxmet 23703 |
. . . 4
β’ (πΈ β (Metβπ) β πΈ β (βMetβπ)) |
11 | 9, 10 | syl 17 |
. . 3
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsxmet 23738 |
. 2
β’ (π β π· β (βMetβπ΅)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsdsf 23736 |
. . . 4
β’ (π β π·:(π΅ Γ π΅)βΆ(0[,]+β)) |
14 | 13 | ffnd 6674 |
. . 3
β’ (π β π· Fn (π΅ Γ π΅)) |
15 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
16 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β πΌ β Fin) |
17 | 8 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ₯ β πΌ π
β π) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ π
β π) |
19 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
20 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
21 | 1, 2, 15, 16, 18, 19, 20, 3, 4, 5 | prdsdsval3 17374 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
22 | 1, 2, 15, 16, 18, 3, 19 | prdsbascl 17372 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
23 | 1, 2, 15, 16, 18, 3, 20 | prdsbascl 17372 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
24 | | r19.26 3115 |
. . . . . . . . . . 11
β’
(βπ₯ β
πΌ ((πβπ₯) β π β§ (πβπ₯) β π) β (βπ₯ β πΌ (πβπ₯) β π β§ βπ₯ β πΌ (πβπ₯) β π)) |
25 | | metcl 23701 |
. . . . . . . . . . . . . . 15
β’ ((πΈ β (Metβπ) β§ (πβπ₯) β π β§ (πβπ₯) β π) β ((πβπ₯)πΈ(πβπ₯)) β β) |
26 | 25 | 3expib 1123 |
. . . . . . . . . . . . . 14
β’ (πΈ β (Metβπ) β (((πβπ₯) β π β§ (πβπ₯) β π) β ((πβπ₯)πΈ(πβπ₯)) β β)) |
27 | 9, 26 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΌ) β (((πβπ₯) β π β§ (πβπ₯) β π) β ((πβπ₯)πΈ(πβπ₯)) β β)) |
28 | 27 | ralimdva 3165 |
. . . . . . . . . . . 12
β’ (π β (βπ₯ β πΌ ((πβπ₯) β π β§ (πβπ₯) β π) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β β)) |
29 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ₯ β πΌ ((πβπ₯) β π β§ (πβπ₯) β π) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β β)) |
30 | 24, 29 | biimtrrid 242 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((βπ₯ β πΌ (πβπ₯) β π β§ βπ₯ β πΌ (πβπ₯) β π) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β β)) |
31 | 22, 23, 30 | mp2and 698 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β β) |
32 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) = (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) |
33 | 32 | fmpt 7063 |
. . . . . . . . 9
β’
(βπ₯ β
πΌ ((πβπ₯)πΈ(πβπ₯)) β β β (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))):πΌβΆβ) |
34 | 31, 33 | sylib 217 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))):πΌβΆβ) |
35 | 34 | frnd 6681 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β β) |
36 | | 0red 11165 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β 0 β β) |
37 | 36 | snssd 4774 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β {0} β
β) |
38 | 35, 37 | unssd 4151 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β) |
39 | | xrltso 13067 |
. . . . . . . 8
β’ < Or
β* |
40 | 39 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β < Or
β*) |
41 | | mptfi 9302 |
. . . . . . . . 9
β’ (πΌ β Fin β (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin) |
42 | | rnfi 9286 |
. . . . . . . . 9
β’ ((π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin) |
43 | 16, 41, 42 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin) |
44 | | snfi 8995 |
. . . . . . . 8
β’ {0}
β Fin |
45 | | unfi 9123 |
. . . . . . . 8
β’ ((ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin β§ {0} β Fin) β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin) |
46 | 43, 44, 45 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin) |
47 | | ssun2 4138 |
. . . . . . . . 9
β’ {0}
β (ran (π₯ β
πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) |
48 | | c0ex 11156 |
. . . . . . . . . 10
β’ 0 β
V |
49 | 48 | snss 4751 |
. . . . . . . . 9
β’ (0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β {0} β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
50 | 47, 49 | mpbir 230 |
. . . . . . . 8
β’ 0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) |
51 | | ne0i 4299 |
. . . . . . . 8
β’ (0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
) |
52 | 50, 51 | mp1i 13 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
) |
53 | | ressxr 11206 |
. . . . . . . 8
β’ β
β β* |
54 | 38, 53 | sstrdi 3961 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
55 | | fisupcl 9412 |
. . . . . . 7
β’ (( <
Or β* β§ ((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin β§ (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
β§ (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β*))
β sup((ran (π₯ β
πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
56 | 40, 46, 52, 54, 55 | syl13anc 1373 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
57 | 38, 56 | sseldd 3950 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β β) |
58 | 21, 57 | eqeltrd 2838 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππ·π) β β) |
59 | 58 | ralrimivva 3198 |
. . 3
β’ (π β βπ β π΅ βπ β π΅ (ππ·π) β β) |
60 | | ffnov 7488 |
. . 3
β’ (π·:(π΅ Γ π΅)βΆβ β (π· Fn (π΅ Γ π΅) β§ βπ β π΅ βπ β π΅ (ππ·π) β β)) |
61 | 14, 59, 60 | sylanbrc 584 |
. 2
β’ (π β π·:(π΅ Γ π΅)βΆβ) |
62 | | ismet2 23702 |
. 2
β’ (π· β (Metβπ΅) β (π· β (βMetβπ΅) β§ π·:(π΅ Γ π΅)βΆβ)) |
63 | 12, 61, 62 | sylanbrc 584 |
1
β’ (π β π· β (Metβπ΅)) |