Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . 4
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | | cnvimass 6037 |
. . . . . . . . 9
β’ (β‘π· β (0[,)π)) β dom π· |
3 | | psmetf 23682 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
4 | 2, 3 | fssdm 6692 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β (β‘π· β (0[,)π)) β (π Γ π)) |
5 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ π β β+) β (β‘π· β (0[,)π)) β (π Γ π)) |
6 | | cnvexg 7865 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β β‘π· β V) |
7 | | imaexg 7856 |
. . . . . . . . 9
β’ (β‘π· β V β (β‘π· β (0[,)π)) β V) |
8 | | elpwg 4567 |
. . . . . . . . 9
β’ ((β‘π· β (0[,)π)) β V β ((β‘π· β (0[,)π)) β π« (π Γ π) β (β‘π· β (0[,)π)) β (π Γ π))) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β ((β‘π· β (0[,)π)) β π« (π Γ π) β (β‘π· β (0[,)π)) β (π Γ π))) |
10 | 9 | ad2antrr 725 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ π β β+) β ((β‘π· β (0[,)π)) β π« (π Γ π) β (β‘π· β (0[,)π)) β (π Γ π))) |
11 | 5, 10 | mpbird 257 |
. . . . . 6
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ π β β+) β (β‘π· β (0[,)π)) β π« (π Γ π)) |
12 | 11 | ralrimiva 3140 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β βπ β β+ (β‘π· β (0[,)π)) β π« (π Γ π)) |
13 | | eqid 2733 |
. . . . . 6
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
14 | 13 | rnmptss 7074 |
. . . . 5
β’
(βπ β
β+ (β‘π· β (0[,)π)) β π« (π Γ π) β ran (π β β+ β¦ (β‘π· β (0[,)π))) β π« (π Γ π)) |
15 | 12, 14 | syl 17 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β ran (π β β+ β¦ (β‘π· β (0[,)π))) β π« (π Γ π)) |
16 | 1, 15 | eqsstrid 3996 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β πΉ β π« (π Γ π)) |
17 | | simpr 486 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β πΉ) |
18 | 16, 17 | sseldd 3949 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β π« (π Γ π)) |
19 | 18 | elpwid 4573 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β (π Γ π)) |