Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β π· β (PsMetβπ)) |
2 | | simp3 1138 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β π β π) |
3 | | simpr 485 |
. . . . 5
β’ ((((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β§ π€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))) β§ π€ β π) β π€ β π) |
4 | | eqid 2732 |
. . . . . . . . 9
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
5 | 4 | elrnmpt 5955 |
. . . . . . . 8
β’ (π€ β V β (π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π€ = (β‘π· β (0[,)π)))) |
6 | 5 | elv 3480 |
. . . . . . 7
β’ (π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
7 | 6 | biimpi 215 |
. . . . . 6
β’ (π€ β ran (π β β+ β¦ (β‘π· β (0[,)π))) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
8 | 7 | ad2antlr 725 |
. . . . 5
β’ ((((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β§ π€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))) β§ π€ β π) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
9 | | sseq1 4007 |
. . . . . . 7
β’ (π€ = (β‘π· β (0[,)π)) β (π€ β π β (β‘π· β (0[,)π)) β π)) |
10 | 9 | biimpcd 248 |
. . . . . 6
β’ (π€ β π β (π€ = (β‘π· β (0[,)π)) β (β‘π· β (0[,)π)) β π)) |
11 | 10 | reximdv 3170 |
. . . . 5
β’ (π€ β π β (βπ β β+ π€ = (β‘π· β (0[,)π)) β βπ β β+ (β‘π· β (0[,)π)) β π)) |
12 | 3, 8, 11 | sylc 65 |
. . . 4
β’ ((((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β§ π€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))) β§ π€ β π) β βπ β β+ (β‘π· β (0[,)π)) β π) |
13 | 2 | ne0d 4335 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β π β β
) |
14 | | simp2 1137 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β π β (metUnifβπ·)) |
15 | | metuel 24080 |
. . . . . 6
β’ ((π β β
β§ π· β (PsMetβπ)) β (π β (metUnifβπ·) β (π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π))) |
16 | 15 | simplbda 500 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π β (metUnifβπ·)) β βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π) |
17 | 13, 1, 14, 16 | syl21anc 836 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π) |
18 | 12, 17 | r19.29a 3162 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ β β+ (β‘π· β (0[,)π)) β π) |
19 | | imass1 6100 |
. . . . . 6
β’ ((β‘π· β (0[,)π)) β π β ((β‘π· β (0[,)π)) β {π}) β (π β {π})) |
20 | 19 | reximi 3084 |
. . . . 5
β’
(βπ β
β+ (β‘π· β (0[,)π)) β π β βπ β β+ ((β‘π· β (0[,)π)) β {π}) β (π β {π})) |
21 | | blval2 24078 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π) = ((β‘π· β (0[,)π)) β {π})) |
22 | 21 | sseq1d 4013 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β ((π(ballβπ·)π) β (π β {π}) β ((β‘π· β (0[,)π)) β {π}) β (π β {π}))) |
23 | 22 | 3expa 1118 |
. . . . . 6
β’ (((π· β (PsMetβπ) β§ π β π) β§ π β β+) β ((π(ballβπ·)π) β (π β {π}) β ((β‘π· β (0[,)π)) β {π}) β (π β {π}))) |
24 | 23 | rexbidva 3176 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β (π β {π}) β βπ β β+ ((β‘π· β (0[,)π)) β {π}) β (π β {π}))) |
25 | 20, 24 | imbitrrid 245 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ β β+ (β‘π· β (0[,)π)) β π β βπ β β+ (π(ballβπ·)π) β (π β {π}))) |
26 | 25 | imp 407 |
. . 3
β’ (((π· β (PsMetβπ) β§ π β π) β§ βπ β β+ (β‘π· β (0[,)π)) β π) β βπ β β+ (π(ballβπ·)π) β (π β {π})) |
27 | 1, 2, 18, 26 | syl21anc 836 |
. 2
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ β β+ (π(ballβπ·)π) β (π β {π})) |
28 | | blssexps 23939 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ β ran (ballβπ·)(π β π β§ π β (π β {π})) β βπ β β+ (π(ballβπ·)π) β (π β {π}))) |
29 | 28 | 3adant2 1131 |
. 2
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β (βπ β ran (ballβπ·)(π β π β§ π β (π β {π})) β βπ β β+ (π(ballβπ·)π) β (π β {π}))) |
30 | 27, 29 | mpbird 256 |
1
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ β ran (ballβπ·)(π β π β§ π β (π β {π}))) |