Step | Hyp | Ref
| Expression |
1 | | rpxr 12983 |
. . 3
β’ (π
β β+
β π
β
β*) |
2 | | blvalps 23891 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β*) β (π(ballβπ·)π
) = {π₯ β π β£ (ππ·π₯) < π
}) |
3 | 1, 2 | syl3an3 1166 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π(ballβπ·)π
) = {π₯ β π β£ (ππ·π₯) < π
}) |
4 | | nfv 1918 |
. . 3
β’
β²π₯(π· β (PsMetβπ) β§ π β π β§ π
β
β+) |
5 | | nfcv 2904 |
. . 3
β’
β²π₯((β‘π· β (0[,)π
)) β {π}) |
6 | | nfrab1 3452 |
. . 3
β’
β²π₯{π₯ β π β£ (ππ·π₯) < π
} |
7 | | psmetf 23812 |
. . . . . . 7
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
8 | | ffn 6718 |
. . . . . . 7
β’ (π·:(π Γ π)βΆβ* β π· Fn (π Γ π)) |
9 | | elpreima 7060 |
. . . . . . 7
β’ (π· Fn (π Γ π) β (β¨π, π₯β© β (β‘π· β (0[,)π
)) β (β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)))) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . 6
β’ (π· β (PsMetβπ) β (β¨π, π₯β© β (β‘π· β (0[,)π
)) β (β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)))) |
11 | 10 | 3ad2ant1 1134 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
(β¨π, π₯β© β (β‘π· β (0[,)π
)) β (β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)))) |
12 | | opelxp 5713 |
. . . . . . . . . 10
β’
(β¨π, π₯β© β (π Γ π) β (π β π β§ π₯ β π)) |
13 | 12 | baib 537 |
. . . . . . . . 9
β’ (π β π β (β¨π, π₯β© β (π Γ π) β π₯ β π)) |
14 | 13 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
(β¨π, π₯β© β (π Γ π) β π₯ β π)) |
15 | 14 | biimpd 228 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
(β¨π, π₯β© β (π Γ π) β π₯ β π)) |
16 | 15 | adantrd 493 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
((β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)) β π₯ β π)) |
17 | | simprl 770 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ (π₯ β π β§ (ππ·π₯) < π
)) β π₯ β π) |
18 | 17 | ex 414 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β ((π₯ β π β§ (ππ·π₯) < π
) β π₯ β π)) |
19 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β π β π) |
20 | 19, 13 | syl 17 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β (β¨π, π₯β© β (π Γ π) β π₯ β π)) |
21 | | df-ov 7412 |
. . . . . . . . . 10
β’ (ππ·π₯) = (π·ββ¨π, π₯β©) |
22 | 21 | eleq1i 2825 |
. . . . . . . . 9
β’ ((ππ·π₯) β (0[,)π
) β (π·ββ¨π, π₯β©) β (0[,)π
)) |
23 | | 0xr 11261 |
. . . . . . . . . . 11
β’ 0 β
β* |
24 | | simpl3 1194 |
. . . . . . . . . . . 12
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β π
β
β+) |
25 | 24 | rpxrd 13017 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β π
β
β*) |
26 | | elico1 13367 |
. . . . . . . . . . 11
β’ ((0
β β* β§ π
β β*) β ((ππ·π₯) β (0[,)π
) β ((ππ·π₯) β β* β§ 0 β€
(ππ·π₯) β§ (ππ·π₯) < π
))) |
27 | 23, 25, 26 | sylancr 588 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((ππ·π₯) β (0[,)π
) β ((ππ·π₯) β β* β§ 0 β€
(ππ·π₯) β§ (ππ·π₯) < π
))) |
28 | | df-3an 1090 |
. . . . . . . . . . 11
β’ (((ππ·π₯) β β* β§ 0 β€
(ππ·π₯) β§ (ππ·π₯) < π
) β (((ππ·π₯) β β* β§ 0 β€
(ππ·π₯)) β§ (ππ·π₯) < π
)) |
29 | | simpl1 1192 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β π· β (PsMetβπ)) |
30 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β π₯ β π) |
31 | | psmetcl 23813 |
. . . . . . . . . . . . . 14
β’ ((π· β (PsMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
32 | 29, 19, 30, 31 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β (ππ·π₯) β
β*) |
33 | | psmetge0 23818 |
. . . . . . . . . . . . . 14
β’ ((π· β (PsMetβπ) β§ π β π β§ π₯ β π) β 0 β€ (ππ·π₯)) |
34 | 29, 19, 30, 33 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β 0 β€ (ππ·π₯)) |
35 | 32, 34 | jca 513 |
. . . . . . . . . . . 12
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((ππ·π₯) β β* β§ 0 β€
(ππ·π₯))) |
36 | 35 | biantrurd 534 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((ππ·π₯) < π
β (((ππ·π₯) β β* β§ 0 β€
(ππ·π₯)) β§ (ππ·π₯) < π
))) |
37 | 28, 36 | bitr4id 290 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β (((ππ·π₯) β β* β§ 0 β€
(ππ·π₯) β§ (ππ·π₯) < π
) β (ππ·π₯) < π
)) |
38 | 27, 37 | bitrd 279 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((ππ·π₯) β (0[,)π
) β (ππ·π₯) < π
)) |
39 | 22, 38 | bitr3id 285 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((π·ββ¨π, π₯β©) β (0[,)π
) β (ππ·π₯) < π
)) |
40 | 20, 39 | anbi12d 632 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π β π β§ π
β β+) β§ π₯ β π) β ((β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)) β (π₯ β π β§ (ππ·π₯) < π
))) |
41 | 40 | ex 414 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π₯ β π β ((β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)) β (π₯ β π β§ (ππ·π₯) < π
)))) |
42 | 16, 18, 41 | pm5.21ndd 381 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
((β¨π, π₯β© β (π Γ π) β§ (π·ββ¨π, π₯β©) β (0[,)π
)) β (π₯ β π β§ (ππ·π₯) < π
))) |
43 | 11, 42 | bitrd 279 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β
(β¨π, π₯β© β (β‘π· β (0[,)π
)) β (π₯ β π β§ (ππ·π₯) < π
))) |
44 | | elimasng 6088 |
. . . . . 6
β’ ((π β π β§ π₯ β V) β (π₯ β ((β‘π· β (0[,)π
)) β {π}) β β¨π, π₯β© β (β‘π· β (0[,)π
)))) |
45 | 44 | elvd 3482 |
. . . . 5
β’ (π β π β (π₯ β ((β‘π· β (0[,)π
)) β {π}) β β¨π, π₯β© β (β‘π· β (0[,)π
)))) |
46 | 45 | 3ad2ant2 1135 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π₯ β ((β‘π· β (0[,)π
)) β {π}) β β¨π, π₯β© β (β‘π· β (0[,)π
)))) |
47 | | rabid 3453 |
. . . . 5
β’ (π₯ β {π₯ β π β£ (ππ·π₯) < π
} β (π₯ β π β§ (ππ·π₯) < π
)) |
48 | 47 | a1i 11 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π₯ β {π₯ β π β£ (ππ·π₯) < π
} β (π₯ β π β§ (ππ·π₯) < π
))) |
49 | 43, 46, 48 | 3bitr4d 311 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π₯ β ((β‘π· β (0[,)π
)) β {π}) β π₯ β {π₯ β π β£ (ππ·π₯) < π
})) |
50 | 4, 5, 6, 49 | eqrd 4002 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β ((β‘π· β (0[,)π
)) β {π}) = {π₯ β π β£ (ππ·π₯) < π
}) |
51 | 3, 50 | eqtr4d 2776 |
1
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β+) β (π(ballβπ·)π
) = ((β‘π· β (0[,)π
)) β {π})) |