Step | Hyp | Ref
| Expression |
1 | | metuel2.u |
. . . 4
β’ π = (metUnifβπ·) |
2 | 1 | eleq2i 2826 |
. . 3
β’ (π β π β π β (metUnifβπ·)) |
3 | 2 | a1i 11 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (π β π β π β (metUnifβπ·))) |
4 | | metuel 24073 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (π β (metUnifβπ·) β (π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π))) |
5 | | oveq2 7417 |
. . . . . . . . . . . . . 14
β’ (π = π β (0[,)π) = (0[,)π)) |
6 | 5 | imaeq2d 6060 |
. . . . . . . . . . . . 13
β’ (π = π β (β‘π· β (0[,)π)) = (β‘π· β (0[,)π))) |
7 | 6 | cbvmptv 5262 |
. . . . . . . . . . . 12
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
8 | 7 | elrnmpt 5956 |
. . . . . . . . . . 11
β’ (π€ β V β (π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π€ = (β‘π· β (0[,)π)))) |
9 | 8 | elv 3481 |
. . . . . . . . . 10
β’ (π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
10 | 9 | anbi1i 625 |
. . . . . . . . 9
β’ ((π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β§ π€ β π) β (βπ β β+ π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
11 | | r19.41v 3189 |
. . . . . . . . 9
β’
(βπ β
β+ (π€ =
(β‘π· β (0[,)π)) β§ π€ β π) β (βπ β β+ π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
12 | 10, 11 | bitr4i 278 |
. . . . . . . 8
β’ ((π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β§ π€ β π) β βπ β β+ (π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
13 | 12 | exbii 1851 |
. . . . . . 7
β’
(βπ€(π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β§ π€ β π) β βπ€βπ β β+ (π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
14 | | df-rex 3072 |
. . . . . . 7
β’
(βπ€ β ran
(π β
β+ β¦ (β‘π· β (0[,)π)))π€ β π β βπ€(π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β§ π€ β π)) |
15 | | rexcom4 3286 |
. . . . . . 7
β’
(βπ β
β+ βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π) β βπ€βπ β β+ (π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
16 | 13, 14, 15 | 3bitr4i 303 |
. . . . . 6
β’
(βπ€ β ran
(π β
β+ β¦ (β‘π· β (0[,)π)))π€ β π β βπ β β+ βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π)) |
17 | | cnvexg 7915 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β β‘π· β V) |
18 | | imaexg 7906 |
. . . . . . . . 9
β’ (β‘π· β V β (β‘π· β (0[,)π)) β V) |
19 | | sseq1 4008 |
. . . . . . . . . 10
β’ (π€ = (β‘π· β (0[,)π)) β (π€ β π β (β‘π· β (0[,)π)) β π)) |
20 | 19 | ceqsexgv 3643 |
. . . . . . . . 9
β’ ((β‘π· β (0[,)π)) β V β (βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π) β (β‘π· β (0[,)π)) β π)) |
21 | 17, 18, 20 | 3syl 18 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β (βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π) β (β‘π· β (0[,)π)) β π)) |
22 | 21 | rexbidv 3179 |
. . . . . . 7
β’ (π· β (PsMetβπ) β (βπ β β+
βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π) β βπ β β+ (β‘π· β (0[,)π)) β π)) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π β (π Γ π)) β (βπ β β+ βπ€(π€ = (β‘π· β (0[,)π)) β§ π€ β π) β βπ β β+ (β‘π· β (0[,)π)) β π)) |
24 | 16, 23 | bitrid 283 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β (π Γ π)) β (βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π β βπ β β+ (β‘π· β (0[,)π)) β π)) |
25 | | cnvimass 6081 |
. . . . . . . . 9
β’ (β‘π· β (0[,)π)) β dom π· |
26 | | simpll 766 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β π· β (PsMetβπ)) |
27 | | psmetf 23812 |
. . . . . . . . . 10
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
28 | | fdm 6727 |
. . . . . . . . . 10
β’ (π·:(π Γ π)βΆβ* β dom
π· = (π Γ π)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β dom π· = (π Γ π)) |
30 | 25, 29 | sseqtrid 4035 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β (β‘π· β (0[,)π)) β (π Γ π)) |
31 | | ssrel2 5786 |
. . . . . . . 8
β’ ((β‘π· β (0[,)π)) β (π Γ π) β ((β‘π· β (0[,)π)) β π β βπ₯ β π βπ¦ β π (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β β¨π₯, π¦β© β π))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β ((β‘π· β (0[,)π)) β π β βπ₯ β π βπ¦ β π (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β β¨π₯, π¦β© β π))) |
33 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β π₯ β π) |
34 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β π¦ β π) |
35 | 33, 34 | opelxpd 5716 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β β¨π₯, π¦β© β (π Γ π)) |
36 | 35 | biantrurd 534 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π·ββ¨π₯, π¦β©) β (0[,)π) β (β¨π₯, π¦β© β (π Γ π) β§ (π·ββ¨π₯, π¦β©) β (0[,)π)))) |
37 | | psmetcl 23813 |
. . . . . . . . . . . . . . 15
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯π·π¦) β
β*) |
38 | 37 | ad5ant145 1370 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β (π₯π·π¦) β
β*) |
39 | 38 | 3biant1d 1479 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((0 β€ (π₯π·π¦) β§ (π₯π·π¦) < π) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦) β§ (π₯π·π¦) < π))) |
40 | | psmetge0 23818 |
. . . . . . . . . . . . . . 15
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯π·π¦)) |
41 | 40 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π¦ β π) β ((π₯π·π¦) < π β (0 β€ (π₯π·π¦) β§ (π₯π·π¦) < π))) |
42 | 41 | ad5ant145 1370 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π₯π·π¦) < π β (0 β€ (π₯π·π¦) β§ (π₯π·π¦) < π))) |
43 | | 0xr 11261 |
. . . . . . . . . . . . . 14
β’ 0 β
β* |
44 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β π β β+) |
45 | 44 | rpxrd 13017 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β π β β*) |
46 | | elico1 13367 |
. . . . . . . . . . . . . 14
β’ ((0
β β* β§ π β β*) β ((π₯π·π¦) β (0[,)π) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦) β§ (π₯π·π¦) < π))) |
47 | 43, 45, 46 | sylancr 588 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π₯π·π¦) β (0[,)π) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦) β§ (π₯π·π¦) < π))) |
48 | 39, 42, 47 | 3bitr4d 311 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π₯π·π¦) < π β (π₯π·π¦) β (0[,)π))) |
49 | | df-ov 7412 |
. . . . . . . . . . . . 13
β’ (π₯π·π¦) = (π·ββ¨π₯, π¦β©) |
50 | 49 | eleq1i 2825 |
. . . . . . . . . . . 12
β’ ((π₯π·π¦) β (0[,)π) β (π·ββ¨π₯, π¦β©) β (0[,)π)) |
51 | 48, 50 | bitrdi 287 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π₯π·π¦) < π β (π·ββ¨π₯, π¦β©) β (0[,)π))) |
52 | | simp-4l 782 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β π· β (PsMetβπ)) |
53 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (π·:(π Γ π)βΆβ* β π· Fn (π Γ π)) |
54 | | elpreima 7060 |
. . . . . . . . . . . 12
β’ (π· Fn (π Γ π) β (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β (β¨π₯, π¦β© β (π Γ π) β§ (π·ββ¨π₯, π¦β©) β (0[,)π)))) |
55 | 52, 27, 53, 54 | 4syl 19 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β (β¨π₯, π¦β© β (π Γ π) β§ (π·ββ¨π₯, π¦β©) β (0[,)π)))) |
56 | 36, 51, 55 | 3bitr4d 311 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ π₯ β π) β§ π¦ β π) β ((π₯π·π¦) < π β β¨π₯, π¦β© β (β‘π· β (0[,)π)))) |
57 | 56 | anasss 468 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) < π β β¨π₯, π¦β© β (β‘π· β (0[,)π)))) |
58 | | df-br 5150 |
. . . . . . . . . 10
β’ (π₯ππ¦ β β¨π₯, π¦β© β π) |
59 | 58 | a1i 11 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦ β β¨π₯, π¦β© β π)) |
60 | 57, 59 | imbi12d 345 |
. . . . . . . 8
β’ ((((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β§ (π₯ β π β§ π¦ β π)) β (((π₯π·π¦) < π β π₯ππ¦) β (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β β¨π₯, π¦β© β π))) |
61 | 60 | 2ralbidva 3217 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β
(βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦) β βπ₯ β π βπ¦ β π (β¨π₯, π¦β© β (β‘π· β (0[,)π)) β β¨π₯, π¦β© β π))) |
62 | 32, 61 | bitr4d 282 |
. . . . . 6
β’ (((π· β (PsMetβπ) β§ π β (π Γ π)) β§ π β β+) β ((β‘π· β (0[,)π)) β π β βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦))) |
63 | 62 | rexbidva 3177 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β (π Γ π)) β (βπ β β+ (β‘π· β (0[,)π)) β π β βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦))) |
64 | 24, 63 | bitrd 279 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β (π Γ π)) β (βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π β βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦))) |
65 | 64 | pm5.32da 580 |
. . 3
β’ (π· β (PsMetβπ) β ((π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π) β (π β (π Γ π) β§ βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦)))) |
66 | 65 | adantl 483 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π) β (π β (π Γ π) β§ βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦)))) |
67 | 3, 4, 66 | 3bitrd 305 |
1
β’ ((π β β
β§ π· β (PsMetβπ)) β (π β π β (π β (π Γ π) β§ βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦)))) |