Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . . . 7
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metustel 23929 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π₯ β πΉ β βπ β β+ π₯ = (β‘π· β (0[,)π)))) |
3 | | simpr 486 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β π₯ = (β‘π· β (0[,)π))) |
4 | | cnvimass 6037 |
. . . . . . . . . 10
β’ (β‘π· β (0[,)π)) β dom π· |
5 | | psmetf 23682 |
. . . . . . . . . . . 12
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
6 | 5 | fdmd 6683 |
. . . . . . . . . . 11
β’ (π· β (PsMetβπ) β dom π· = (π Γ π)) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β dom π· = (π Γ π)) |
8 | 4, 7 | sseqtrid 4000 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β (β‘π· β (0[,)π)) β (π Γ π)) |
9 | 3, 8 | eqsstrd 3986 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β π₯ β (π Γ π)) |
10 | 9 | ex 414 |
. . . . . . 7
β’ (π· β (PsMetβπ) β (π₯ = (β‘π· β (0[,)π)) β π₯ β (π Γ π))) |
11 | 10 | rexlimdvw 3154 |
. . . . . 6
β’ (π· β (PsMetβπ) β (βπ β β+
π₯ = (β‘π· β (0[,)π)) β π₯ β (π Γ π))) |
12 | 2, 11 | sylbid 239 |
. . . . 5
β’ (π· β (PsMetβπ) β (π₯ β πΉ β π₯ β (π Γ π))) |
13 | 12 | ralrimiv 3139 |
. . . 4
β’ (π· β (PsMetβπ) β βπ₯ β πΉ π₯ β (π Γ π)) |
14 | | pwssb 5065 |
. . . 4
β’ (πΉ β π« (π Γ π) β βπ₯ β πΉ π₯ β (π Γ π)) |
15 | 13, 14 | sylibr 233 |
. . 3
β’ (π· β (PsMetβπ) β πΉ β π« (π Γ π)) |
16 | 15 | adantl 483 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β π« (π Γ π)) |
17 | | cnvexg 7865 |
. . . . . . 7
β’ (π· β (PsMetβπ) β β‘π· β V) |
18 | | imaexg 7856 |
. . . . . . 7
β’ (β‘π· β V β (β‘π· β (0[,)1)) β V) |
19 | | elisset 2816 |
. . . . . . 7
β’ ((β‘π· β (0[,)1)) β V β
βπ₯ π₯ = (β‘π· β (0[,)1))) |
20 | | 1rp 12927 |
. . . . . . . . 9
β’ 1 β
β+ |
21 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π = 1 β (0[,)π) = (0[,)1)) |
22 | 21 | imaeq2d 6017 |
. . . . . . . . . 10
β’ (π = 1 β (β‘π· β (0[,)π)) = (β‘π· β (0[,)1))) |
23 | 22 | rspceeqv 3599 |
. . . . . . . . 9
β’ ((1
β β+ β§ π₯ = (β‘π· β (0[,)1))) β βπ β β+
π₯ = (β‘π· β (0[,)π))) |
24 | 20, 23 | mpan 689 |
. . . . . . . 8
β’ (π₯ = (β‘π· β (0[,)1)) β βπ β β+
π₯ = (β‘π· β (0[,)π))) |
25 | 24 | eximi 1838 |
. . . . . . 7
β’
(βπ₯ π₯ = (β‘π· β (0[,)1)) β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π))) |
26 | 17, 18, 19, 25 | 4syl 19 |
. . . . . 6
β’ (π· β (PsMetβπ) β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π))) |
27 | 2 | exbidv 1925 |
. . . . . 6
β’ (π· β (PsMetβπ) β (βπ₯ π₯ β πΉ β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π)))) |
28 | 26, 27 | mpbird 257 |
. . . . 5
β’ (π· β (PsMetβπ) β βπ₯ π₯ β πΉ) |
29 | 28 | adantl 483 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ₯ π₯ β πΉ) |
30 | | n0 4310 |
. . . 4
β’ (πΉ β β
β
βπ₯ π₯ β πΉ) |
31 | 29, 30 | sylibr 233 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β β
) |
32 | 1 | metustid 23933 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β πΉ) β ( I βΎ π) β π₯) |
33 | 32 | adantll 713 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β ( I βΎ π) β π₯) |
34 | | n0 4310 |
. . . . . . . . . 10
β’ (π β β
β
βπ π β π) |
35 | 34 | biimpi 215 |
. . . . . . . . 9
β’ (π β β
β
βπ π β π) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ π β π) |
37 | | opelidres 5953 |
. . . . . . . . . . 11
β’ (π β π β (β¨π, πβ© β ( I βΎ π) β π β π)) |
38 | 37 | ibir 268 |
. . . . . . . . . 10
β’ (π β π β β¨π, πβ© β ( I βΎ π)) |
39 | 38 | ne0d 4299 |
. . . . . . . . 9
β’ (π β π β ( I βΎ π) β β
) |
40 | 39 | exlimiv 1934 |
. . . . . . . 8
β’
(βπ π β π β ( I βΎ π) β β
) |
41 | 36, 40 | syl 17 |
. . . . . . 7
β’ ((π β β
β§ π· β (PsMetβπ)) β ( I βΎ π) β β
) |
42 | 41 | adantr 482 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β ( I βΎ π) β β
) |
43 | | ssn0 4364 |
. . . . . 6
β’ ((( I
βΎ π) β π₯ β§ ( I βΎ π) β β
) β π₯ β β
) |
44 | 33, 42, 43 | syl2anc 585 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β π₯ β β
) |
45 | 44 | nelrdva 3667 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β Β¬ β
β
πΉ) |
46 | | df-nel 3047 |
. . . 4
β’ (β
β πΉ β Β¬
β
β πΉ) |
47 | 45, 46 | sylibr 233 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β β
β πΉ) |
48 | | df-ss 3931 |
. . . . . . . . 9
β’ (π₯ β π¦ β (π₯ β© π¦) = π₯) |
49 | 48 | biimpi 215 |
. . . . . . . 8
β’ (π₯ β π¦ β (π₯ β© π¦) = π₯) |
50 | 49 | adantl 483 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β (π₯ β© π¦) = π₯) |
51 | | simplrl 776 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β π₯ β πΉ) |
52 | 50, 51 | eqeltrd 2834 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β (π₯ β© π¦) β πΉ) |
53 | | sseqin2 4179 |
. . . . . . . . 9
β’ (π¦ β π₯ β (π₯ β© π¦) = π¦) |
54 | 53 | biimpi 215 |
. . . . . . . 8
β’ (π¦ β π₯ β (π₯ β© π¦) = π¦) |
55 | 54 | adantl 483 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β (π₯ β© π¦) = π¦) |
56 | | simplrr 777 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β π¦ β πΉ) |
57 | 55, 56 | eqeltrd 2834 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β (π₯ β© π¦) β πΉ) |
58 | | simplr 768 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π· β (PsMetβπ)) |
59 | | simprl 770 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π₯ β πΉ) |
60 | | simprr 772 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π¦ β πΉ) |
61 | 1 | metustto 23932 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β πΉ β§ π¦ β πΉ) β (π₯ β π¦ β¨ π¦ β π₯)) |
62 | 58, 59, 60, 61 | syl3anc 1372 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β π¦ β¨ π¦ β π₯)) |
63 | 52, 57, 62 | mpjaodan 958 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β© π¦) β πΉ) |
64 | | ssidd 3971 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β© π¦) β (π₯ β© π¦)) |
65 | | sseq1 3973 |
. . . . . 6
β’ (π§ = (π₯ β© π¦) β (π§ β (π₯ β© π¦) β (π₯ β© π¦) β (π₯ β© π¦))) |
66 | 65 | rspcev 3583 |
. . . . 5
β’ (((π₯ β© π¦) β πΉ β§ (π₯ β© π¦) β (π₯ β© π¦)) β βπ§ β πΉ π§ β (π₯ β© π¦)) |
67 | 63, 64, 66 | syl2anc 585 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β βπ§ β πΉ π§ β (π₯ β© π¦)) |
68 | 67 | ralrimivva 3194 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦)) |
69 | 31, 47, 68 | 3jca 1129 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))) |
70 | | elfvex 6884 |
. . . . 5
β’ (π· β (PsMetβπ) β π β V) |
71 | 70 | adantl 483 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β π β V) |
72 | 71, 71 | xpexd 7689 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β (π Γ π) β V) |
73 | | isfbas2 23209 |
. . 3
β’ ((π Γ π) β V β (πΉ β (fBasβ(π Γ π)) β (πΉ β π« (π Γ π) β§ (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))))) |
74 | 72, 73 | syl 17 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (πΉ β (fBasβ(π Γ π)) β (πΉ β π« (π Γ π) β§ (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))))) |
75 | 16, 69, 74 | mpbir2and 712 |
1
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) |