Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . . . 7
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metustel 24058 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π₯ β πΉ β βπ β β+ π₯ = (β‘π· β (0[,)π)))) |
3 | | simpr 485 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β π₯ = (β‘π· β (0[,)π))) |
4 | | cnvimass 6080 |
. . . . . . . . . 10
β’ (β‘π· β (0[,)π)) β dom π· |
5 | | psmetf 23811 |
. . . . . . . . . . . 12
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
6 | 5 | fdmd 6728 |
. . . . . . . . . . 11
β’ (π· β (PsMetβπ) β dom π· = (π Γ π)) |
7 | 6 | adantr 481 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β dom π· = (π Γ π)) |
8 | 4, 7 | sseqtrid 4034 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β (β‘π· β (0[,)π)) β (π Γ π)) |
9 | 3, 8 | eqsstrd 4020 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π₯ = (β‘π· β (0[,)π))) β π₯ β (π Γ π)) |
10 | 9 | ex 413 |
. . . . . . 7
β’ (π· β (PsMetβπ) β (π₯ = (β‘π· β (0[,)π)) β π₯ β (π Γ π))) |
11 | 10 | rexlimdvw 3160 |
. . . . . 6
β’ (π· β (PsMetβπ) β (βπ β β+
π₯ = (β‘π· β (0[,)π)) β π₯ β (π Γ π))) |
12 | 2, 11 | sylbid 239 |
. . . . 5
β’ (π· β (PsMetβπ) β (π₯ β πΉ β π₯ β (π Γ π))) |
13 | 12 | ralrimiv 3145 |
. . . 4
β’ (π· β (PsMetβπ) β βπ₯ β πΉ π₯ β (π Γ π)) |
14 | | pwssb 5104 |
. . . 4
β’ (πΉ β π« (π Γ π) β βπ₯ β πΉ π₯ β (π Γ π)) |
15 | 13, 14 | sylibr 233 |
. . 3
β’ (π· β (PsMetβπ) β πΉ β π« (π Γ π)) |
16 | 15 | adantl 482 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β π« (π Γ π)) |
17 | | cnvexg 7914 |
. . . . . . 7
β’ (π· β (PsMetβπ) β β‘π· β V) |
18 | | imaexg 7905 |
. . . . . . 7
β’ (β‘π· β V β (β‘π· β (0[,)1)) β V) |
19 | | elisset 2815 |
. . . . . . 7
β’ ((β‘π· β (0[,)1)) β V β
βπ₯ π₯ = (β‘π· β (0[,)1))) |
20 | | 1rp 12977 |
. . . . . . . . 9
β’ 1 β
β+ |
21 | | oveq2 7416 |
. . . . . . . . . . 11
β’ (π = 1 β (0[,)π) = (0[,)1)) |
22 | 21 | imaeq2d 6059 |
. . . . . . . . . 10
β’ (π = 1 β (β‘π· β (0[,)π)) = (β‘π· β (0[,)1))) |
23 | 22 | rspceeqv 3633 |
. . . . . . . . 9
β’ ((1
β β+ β§ π₯ = (β‘π· β (0[,)1))) β βπ β β+
π₯ = (β‘π· β (0[,)π))) |
24 | 20, 23 | mpan 688 |
. . . . . . . 8
β’ (π₯ = (β‘π· β (0[,)1)) β βπ β β+
π₯ = (β‘π· β (0[,)π))) |
25 | 24 | eximi 1837 |
. . . . . . 7
β’
(βπ₯ π₯ = (β‘π· β (0[,)1)) β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π))) |
26 | 17, 18, 19, 25 | 4syl 19 |
. . . . . 6
β’ (π· β (PsMetβπ) β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π))) |
27 | 2 | exbidv 1924 |
. . . . . 6
β’ (π· β (PsMetβπ) β (βπ₯ π₯ β πΉ β βπ₯βπ β β+ π₯ = (β‘π· β (0[,)π)))) |
28 | 26, 27 | mpbird 256 |
. . . . 5
β’ (π· β (PsMetβπ) β βπ₯ π₯ β πΉ) |
29 | 28 | adantl 482 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ₯ π₯ β πΉ) |
30 | | n0 4346 |
. . . 4
β’ (πΉ β β
β
βπ₯ π₯ β πΉ) |
31 | 29, 30 | sylibr 233 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β β
) |
32 | 1 | metustid 24062 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β πΉ) β ( I βΎ π) β π₯) |
33 | 32 | adantll 712 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β ( I βΎ π) β π₯) |
34 | | n0 4346 |
. . . . . . . . . 10
β’ (π β β
β
βπ π β π) |
35 | 34 | biimpi 215 |
. . . . . . . . 9
β’ (π β β
β
βπ π β π) |
36 | 35 | adantr 481 |
. . . . . . . 8
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ π β π) |
37 | | opelidres 5993 |
. . . . . . . . . . 11
β’ (π β π β (β¨π, πβ© β ( I βΎ π) β π β π)) |
38 | 37 | ibir 267 |
. . . . . . . . . 10
β’ (π β π β β¨π, πβ© β ( I βΎ π)) |
39 | 38 | ne0d 4335 |
. . . . . . . . 9
β’ (π β π β ( I βΎ π) β β
) |
40 | 39 | exlimiv 1933 |
. . . . . . . 8
β’
(βπ π β π β ( I βΎ π) β β
) |
41 | 36, 40 | syl 17 |
. . . . . . 7
β’ ((π β β
β§ π· β (PsMetβπ)) β ( I βΎ π) β β
) |
42 | 41 | adantr 481 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β ( I βΎ π) β β
) |
43 | | ssn0 4400 |
. . . . . 6
β’ ((( I
βΎ π) β π₯ β§ ( I βΎ π) β β
) β π₯ β β
) |
44 | 33, 42, 43 | syl2anc 584 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π₯ β πΉ) β π₯ β β
) |
45 | 44 | nelrdva 3701 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β Β¬ β
β
πΉ) |
46 | | df-nel 3047 |
. . . 4
β’ (β
β πΉ β Β¬
β
β πΉ) |
47 | 45, 46 | sylibr 233 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β β
β πΉ) |
48 | | df-ss 3965 |
. . . . . . . . 9
β’ (π₯ β π¦ β (π₯ β© π¦) = π₯) |
49 | 48 | biimpi 215 |
. . . . . . . 8
β’ (π₯ β π¦ β (π₯ β© π¦) = π₯) |
50 | 49 | adantl 482 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β (π₯ β© π¦) = π₯) |
51 | | simplrl 775 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β π₯ β πΉ) |
52 | 50, 51 | eqeltrd 2833 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π₯ β π¦) β (π₯ β© π¦) β πΉ) |
53 | | sseqin2 4215 |
. . . . . . . . 9
β’ (π¦ β π₯ β (π₯ β© π¦) = π¦) |
54 | 53 | biimpi 215 |
. . . . . . . 8
β’ (π¦ β π₯ β (π₯ β© π¦) = π¦) |
55 | 54 | adantl 482 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β (π₯ β© π¦) = π¦) |
56 | | simplrr 776 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β π¦ β πΉ) |
57 | 55, 56 | eqeltrd 2833 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β§ π¦ β π₯) β (π₯ β© π¦) β πΉ) |
58 | | simplr 767 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π· β (PsMetβπ)) |
59 | | simprl 769 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π₯ β πΉ) |
60 | | simprr 771 |
. . . . . . 7
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β π¦ β πΉ) |
61 | 1 | metustto 24061 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β πΉ β§ π¦ β πΉ) β (π₯ β π¦ β¨ π¦ β π₯)) |
62 | 58, 59, 60, 61 | syl3anc 1371 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β π¦ β¨ π¦ β π₯)) |
63 | 52, 57, 62 | mpjaodan 957 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β© π¦) β πΉ) |
64 | | ssidd 4005 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β (π₯ β© π¦) β (π₯ β© π¦)) |
65 | | sseq1 4007 |
. . . . . 6
β’ (π§ = (π₯ β© π¦) β (π§ β (π₯ β© π¦) β (π₯ β© π¦) β (π₯ β© π¦))) |
66 | 65 | rspcev 3612 |
. . . . 5
β’ (((π₯ β© π¦) β πΉ β§ (π₯ β© π¦) β (π₯ β© π¦)) β βπ§ β πΉ π§ β (π₯ β© π¦)) |
67 | 63, 64, 66 | syl2anc 584 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π₯ β πΉ β§ π¦ β πΉ)) β βπ§ β πΉ π§ β (π₯ β© π¦)) |
68 | 67 | ralrimivva 3200 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦)) |
69 | 31, 47, 68 | 3jca 1128 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))) |
70 | | elfvex 6929 |
. . . . 5
β’ (π· β (PsMetβπ) β π β V) |
71 | 70 | adantl 482 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β π β V) |
72 | 71, 71 | xpexd 7737 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β (π Γ π) β V) |
73 | | isfbas2 23338 |
. . 3
β’ ((π Γ π) β V β (πΉ β (fBasβ(π Γ π)) β (πΉ β π« (π Γ π) β§ (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))))) |
74 | 72, 73 | syl 17 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (πΉ β (fBasβ(π Γ π)) β (πΉ β π« (π Γ π) β§ (πΉ β β
β§ β
β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))))) |
75 | 16, 69, 74 | mpbir2and 711 |
1
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) |