Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . 4
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metustss 23930 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β (π Γ π)) |
3 | | cnvss 5832 |
. . . 4
β’ (π΄ β (π Γ π) β β‘π΄ β β‘(π Γ π)) |
4 | | cnvxp 6113 |
. . . 4
β’ β‘(π Γ π) = (π Γ π) |
5 | 3, 4 | sseqtrdi 3998 |
. . 3
β’ (π΄ β (π Γ π) β β‘π΄ β (π Γ π)) |
6 | 2, 5 | syl 17 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ β (π Γ π)) |
7 | | simp-4l 782 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π· β (PsMetβπ)) |
8 | | simpr1r 1232 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ ((π β π β§ π β π) β§ π β β+ β§ π΄ = (β‘π· β (0[,)π)))) β π β π) |
9 | 8 | 3anassrs 1361 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π β π) |
10 | | simpr1l 1231 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ ((π β π β§ π β π) β§ π β β+ β§ π΄ = (β‘π· β (0[,)π)))) β π β π) |
11 | 10 | 3anassrs 1361 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π β π) |
12 | | psmetsym 23686 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π β π β§ π β π) β (ππ·π) = (ππ·π)) |
13 | 7, 9, 11, 12 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (ππ·π) = (ππ·π)) |
14 | | df-ov 7364 |
. . . . . . . . 9
β’ (ππ·π) = (π·ββ¨π, πβ©) |
15 | | df-ov 7364 |
. . . . . . . . 9
β’ (ππ·π) = (π·ββ¨π, πβ©) |
16 | 13, 14, 15 | 3eqtr3g 2796 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π·ββ¨π, πβ©) = (π·ββ¨π, πβ©)) |
17 | 16 | eleq1d 2819 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β (π·ββ¨π, πβ©) β (0[,)π))) |
18 | | psmetf 23682 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
19 | | ffun 6675 |
. . . . . . . . 9
β’ (π·:(π Γ π)βΆβ* β Fun
π·) |
20 | 7, 18, 19 | 3syl 18 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β Fun π·) |
21 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π β π β§ π β π)) |
22 | 21 | ancomd 463 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π β π β§ π β π)) |
23 | | opelxpi 5674 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β (π Γ π)) |
25 | | fdm 6681 |
. . . . . . . . . 10
β’ (π·:(π Γ π)βΆβ* β dom
π· = (π Γ π)) |
26 | 7, 18, 25 | 3syl 18 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β dom π· = (π Γ π)) |
27 | 24, 26 | eleqtrrd 2837 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β dom π·) |
28 | | fvimacnv 7007 |
. . . . . . . 8
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
29 | 20, 27, 28 | syl2anc 585 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
30 | | opelxpi 5674 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
31 | 21, 30 | syl 17 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β (π Γ π)) |
32 | 31, 26 | eleqtrrd 2837 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β dom π·) |
33 | | fvimacnv 7007 |
. . . . . . . 8
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
34 | 20, 32, 33 | syl2anc 585 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
35 | 17, 29, 34 | 3bitr3d 309 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β (β‘π· β (0[,)π)) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
36 | | simpr 486 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π΄ = (β‘π· β (0[,)π))) |
37 | 36 | eleq2d 2820 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β (β‘π· β (0[,)π)))) |
38 | 36 | eleq2d 2820 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β (β‘π· β (0[,)π)))) |
39 | 35, 37, 38 | 3bitr4d 311 |
. . . . 5
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β π΄)) |
40 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
41 | 40 | elrnmpt 5915 |
. . . . . . . 8
β’ (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
42 | 41 | ibi 267 |
. . . . . . 7
β’ (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
43 | 42, 1 | eleq2s 2852 |
. . . . . 6
β’ (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
44 | 43 | ad2antlr 726 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
45 | 39, 44 | r19.29a 3156 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β (β¨π, πβ© β π΄ β β¨π, πβ© β π΄)) |
46 | | df-br 5110 |
. . . . 5
β’ (πβ‘π΄π β β¨π, πβ© β β‘π΄) |
47 | | vex 3451 |
. . . . . 6
β’ π β V |
48 | | vex 3451 |
. . . . . 6
β’ π β V |
49 | 47, 48 | opelcnv 5841 |
. . . . 5
β’
(β¨π, πβ© β β‘π΄ β β¨π, πβ© β π΄) |
50 | 46, 49 | bitri 275 |
. . . 4
β’ (πβ‘π΄π β β¨π, πβ© β π΄) |
51 | | df-br 5110 |
. . . 4
β’ (ππ΄π β β¨π, πβ© β π΄) |
52 | 45, 50, 51 | 3bitr4g 314 |
. . 3
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β (πβ‘π΄π β ππ΄π)) |
53 | 52 | 3impb 1116 |
. 2
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ π β π β§ π β π) β (πβ‘π΄π β ππ΄π)) |
54 | 6, 2, 53 | eqbrrdva 5829 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ = π΄) |