Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . 4
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metustss 24059 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β (π Γ π)) |
3 | | cnvss 5872 |
. . . 4
β’ (π΄ β (π Γ π) β β‘π΄ β β‘(π Γ π)) |
4 | | cnvxp 6156 |
. . . 4
β’ β‘(π Γ π) = (π Γ π) |
5 | 3, 4 | sseqtrdi 4032 |
. . 3
β’ (π΄ β (π Γ π) β β‘π΄ β (π Γ π)) |
6 | 2, 5 | syl 17 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ β (π Γ π)) |
7 | | simp-4l 781 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π· β (PsMetβπ)) |
8 | | simpr1r 1231 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ ((π β π β§ π β π) β§ π β β+ β§ π΄ = (β‘π· β (0[,)π)))) β π β π) |
9 | 8 | 3anassrs 1360 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π β π) |
10 | | simpr1l 1230 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ ((π β π β§ π β π) β§ π β β+ β§ π΄ = (β‘π· β (0[,)π)))) β π β π) |
11 | 10 | 3anassrs 1360 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π β π) |
12 | | psmetsym 23815 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π β π β§ π β π) β (ππ·π) = (ππ·π)) |
13 | 7, 9, 11, 12 | syl3anc 1371 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (ππ·π) = (ππ·π)) |
14 | | df-ov 7411 |
. . . . . . . . 9
β’ (ππ·π) = (π·ββ¨π, πβ©) |
15 | | df-ov 7411 |
. . . . . . . . 9
β’ (ππ·π) = (π·ββ¨π, πβ©) |
16 | 13, 14, 15 | 3eqtr3g 2795 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π·ββ¨π, πβ©) = (π·ββ¨π, πβ©)) |
17 | 16 | eleq1d 2818 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β (π·ββ¨π, πβ©) β (0[,)π))) |
18 | | psmetf 23811 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
19 | | ffun 6720 |
. . . . . . . . 9
β’ (π·:(π Γ π)βΆβ* β Fun
π·) |
20 | 7, 18, 19 | 3syl 18 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β Fun π·) |
21 | | simpllr 774 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π β π β§ π β π)) |
22 | 21 | ancomd 462 |
. . . . . . . . . 10
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π β π β§ π β π)) |
23 | | opelxpi 5713 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β (π Γ π)) |
25 | | fdm 6726 |
. . . . . . . . . 10
β’ (π·:(π Γ π)βΆβ* β dom
π· = (π Γ π)) |
26 | 7, 18, 25 | 3syl 18 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β dom π· = (π Γ π)) |
27 | 24, 26 | eleqtrrd 2836 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β dom π·) |
28 | | fvimacnv 7054 |
. . . . . . . 8
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
29 | 20, 27, 28 | syl2anc 584 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
30 | | opelxpi 5713 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
31 | 21, 30 | syl 17 |
. . . . . . . . 9
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β (π Γ π)) |
32 | 31, 26 | eleqtrrd 2836 |
. . . . . . . 8
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β dom π·) |
33 | | fvimacnv 7054 |
. . . . . . . 8
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
34 | 20, 32, 33 | syl2anc 584 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
35 | 17, 29, 34 | 3bitr3d 308 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β (β‘π· β (0[,)π)) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
36 | | simpr 485 |
. . . . . . 7
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π΄ = (β‘π· β (0[,)π))) |
37 | 36 | eleq2d 2819 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β (β‘π· β (0[,)π)))) |
38 | 36 | eleq2d 2819 |
. . . . . 6
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β (β‘π· β (0[,)π)))) |
39 | 35, 37, 38 | 3bitr4d 310 |
. . . . 5
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β π΄ β β¨π, πβ© β π΄)) |
40 | | eqid 2732 |
. . . . . . . . 9
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
41 | 40 | elrnmpt 5955 |
. . . . . . . 8
β’ (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
42 | 41 | ibi 266 |
. . . . . . 7
β’ (π΄ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
43 | 42, 1 | eleq2s 2851 |
. . . . . 6
β’ (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
44 | 43 | ad2antlr 725 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
45 | 39, 44 | r19.29a 3162 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β (β¨π, πβ© β π΄ β β¨π, πβ© β π΄)) |
46 | | df-br 5149 |
. . . . 5
β’ (πβ‘π΄π β β¨π, πβ© β β‘π΄) |
47 | | vex 3478 |
. . . . . 6
β’ π β V |
48 | | vex 3478 |
. . . . . 6
β’ π β V |
49 | 47, 48 | opelcnv 5881 |
. . . . 5
β’
(β¨π, πβ© β β‘π΄ β β¨π, πβ© β π΄) |
50 | 46, 49 | bitri 274 |
. . . 4
β’ (πβ‘π΄π β β¨π, πβ© β π΄) |
51 | | df-br 5149 |
. . . 4
β’ (ππ΄π β β¨π, πβ© β π΄) |
52 | 45, 50, 51 | 3bitr4g 313 |
. . 3
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ (π β π β§ π β π)) β (πβ‘π΄π β ππ΄π)) |
53 | 52 | 3impb 1115 |
. 2
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ π β π β§ π β π) β (πβ‘π΄π β ππ΄π)) |
54 | 6, 2, 53 | eqbrrdva 5869 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ = π΄) |