Step | Hyp | Ref
| Expression |
1 | | imassrn 6064 |
. . . . 5
β’ (πΉ β (π(ballβπ)π
)) β ran πΉ |
2 | | isismty 37182 |
. . . . . . . . . 10
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
3 | 2 | biimp3a 1465 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
4 | 3 | adantr 480 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
5 | 4 | simpld 494 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β πΉ:πβ1-1-ontoβπ) |
6 | | f1of 6827 |
. . . . . . 7
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβΆπ) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β πΉ:πβΆπ) |
8 | 7 | frnd 6719 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β ran
πΉ β π) |
9 | 1, 8 | sstrid 3988 |
. . . 4
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (πΉ β (π(ballβπ)π
)) β π) |
10 | 9 | sseld 3976 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (π₯ β (πΉ β (π(ballβπ)π
)) β π₯ β π)) |
11 | | simpl2 1189 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β π β (βMetβπ)) |
12 | | simprl 768 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β π β π) |
13 | | ffvelcdm 7077 |
. . . . . 6
β’ ((πΉ:πβΆπ β§ π β π) β (πΉβπ) β π) |
14 | 7, 12, 13 | syl2anc 583 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (πΉβπ) β π) |
15 | | simprr 770 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β π
β
β*) |
16 | | blssm 24279 |
. . . . 5
β’ ((π β (βMetβπ) β§ (πΉβπ) β π β§ π
β β*) β ((πΉβπ)(ballβπ)π
) β π) |
17 | 11, 14, 15, 16 | syl3anc 1368 |
. . . 4
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β ((πΉβπ)(ballβπ)π
) β π) |
18 | 17 | sseld 3976 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (π₯ β ((πΉβπ)(ballβπ)π
) β π₯ β π)) |
19 | | simpl1 1188 |
. . . . . . . . 9
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β π β (βMetβπ)) |
20 | 19 | adantr 480 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β π β (βMetβπ)) |
21 | | simplrr 775 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β π
β
β*) |
22 | | simplrl 774 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β π β π) |
23 | | f1ocnv 6839 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
24 | | f1of 6827 |
. . . . . . . . . 10
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
25 | 5, 23, 24 | 3syl 18 |
. . . . . . . . 9
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β β‘πΉ:πβΆπ) |
26 | | ffvelcdm 7077 |
. . . . . . . . 9
β’ ((β‘πΉ:πβΆπ β§ π₯ β π) β (β‘πΉβπ₯) β π) |
27 | 25, 26 | sylan 579 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (β‘πΉβπ₯) β π) |
28 | | elbl2 24251 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π
β β*) β§ (π β π β§ (β‘πΉβπ₯) β π)) β ((β‘πΉβπ₯) β (π(ballβπ)π
) β (ππ(β‘πΉβπ₯)) < π
)) |
29 | 20, 21, 22, 27, 28 | syl22anc 836 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((β‘πΉβπ₯) β (π(ballβπ)π
) β (ππ(β‘πΉβπ₯)) < π
)) |
30 | 4 | simprd 495 |
. . . . . . . . . . 11
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β
βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) |
31 | | oveq1 7412 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ππ¦) = (πππ¦)) |
32 | | fveq2 6885 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
33 | 32 | oveq1d 7420 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((πΉβπ₯)π(πΉβπ¦)) = ((πΉβπ)π(πΉβπ¦))) |
34 | 31, 33 | eqeq12d 2742 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β (πππ¦) = ((πΉβπ)π(πΉβπ¦)))) |
35 | | oveq2 7413 |
. . . . . . . . . . . . . 14
β’ (π¦ = (β‘πΉβπ₯) β (πππ¦) = (ππ(β‘πΉβπ₯))) |
36 | | fveq2 6885 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (β‘πΉβπ₯) β (πΉβπ¦) = (πΉβ(β‘πΉβπ₯))) |
37 | 36 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ (π¦ = (β‘πΉβπ₯) β ((πΉβπ)π(πΉβπ¦)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯)))) |
38 | 35, 37 | eqeq12d 2742 |
. . . . . . . . . . . . 13
β’ (π¦ = (β‘πΉβπ₯) β ((πππ¦) = ((πΉβπ)π(πΉβπ¦)) β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯))))) |
39 | 34, 38 | rspc2v 3617 |
. . . . . . . . . . . 12
β’ ((π β π β§ (β‘πΉβπ₯) β π) β (βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯))))) |
40 | 39 | impancom 451 |
. . . . . . . . . . 11
β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β ((β‘πΉβπ₯) β π β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯))))) |
41 | 12, 30, 40 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β ((β‘πΉβπ₯) β π β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯))))) |
42 | 41 | imp 406 |
. . . . . . . . 9
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ (β‘πΉβπ₯) β π) β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯)))) |
43 | 27, 42 | syldan 590 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (ππ(β‘πΉβπ₯)) = ((πΉβπ)π(πΉβ(β‘πΉβπ₯)))) |
44 | 43 | breq1d 5151 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((ππ(β‘πΉβπ₯)) < π
β ((πΉβπ)π(πΉβ(β‘πΉβπ₯))) < π
)) |
45 | 29, 44 | bitrd 279 |
. . . . . 6
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((β‘πΉβπ₯) β (π(ballβπ)π
) β ((πΉβπ)π(πΉβ(β‘πΉβπ₯))) < π
)) |
46 | | f1of1 6826 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβ1-1βπ) |
47 | 5, 46 | syl 17 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β πΉ:πβ1-1βπ) |
48 | 47 | adantr 480 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β πΉ:πβ1-1βπ) |
49 | | blssm 24279 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π β π β§ π
β β*) β (π(ballβπ)π
) β π) |
50 | 19, 12, 15, 49 | syl3anc 1368 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (π(ballβπ)π
) β π) |
51 | 50 | adantr 480 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (π(ballβπ)π
) β π) |
52 | | f1elima 7258 |
. . . . . . 7
β’ ((πΉ:πβ1-1βπ β§ (β‘πΉβπ₯) β π β§ (π(ballβπ)π
) β π) β ((πΉβ(β‘πΉβπ₯)) β (πΉ β (π(ballβπ)π
)) β (β‘πΉβπ₯) β (π(ballβπ)π
))) |
53 | 48, 27, 51, 52 | syl3anc 1368 |
. . . . . 6
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β (πΉ β (π(ballβπ)π
)) β (β‘πΉβπ₯) β (π(ballβπ)π
))) |
54 | 11 | adantr 480 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β π β (βMetβπ)) |
55 | 14 | adantr 480 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (πΉβπ) β π) |
56 | | f1ocnvfv2 7271 |
. . . . . . . . 9
β’ ((πΉ:πβ1-1-ontoβπ β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) = π₯) |
57 | 5, 56 | sylan 579 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) = π₯) |
58 | | simpr 484 |
. . . . . . . 8
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β π₯ β π) |
59 | 57, 58 | eqeltrd 2827 |
. . . . . . 7
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) β π) |
60 | | elbl2 24251 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π
β β*) β§ ((πΉβπ) β π β§ (πΉβ(β‘πΉβπ₯)) β π)) β ((πΉβ(β‘πΉβπ₯)) β ((πΉβπ)(ballβπ)π
) β ((πΉβπ)π(πΉβ(β‘πΉβπ₯))) < π
)) |
61 | 54, 21, 55, 59, 60 | syl22anc 836 |
. . . . . 6
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β ((πΉβπ)(ballβπ)π
) β ((πΉβπ)π(πΉβ(β‘πΉβπ₯))) < π
)) |
62 | 45, 53, 61 | 3bitr4d 311 |
. . . . 5
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β (πΉ β (π(ballβπ)π
)) β (πΉβ(β‘πΉβπ₯)) β ((πΉβπ)(ballβπ)π
))) |
63 | 57 | eleq1d 2812 |
. . . . 5
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β (πΉ β (π(ballβπ)π
)) β π₯ β (πΉ β (π(ballβπ)π
)))) |
64 | 57 | eleq1d 2812 |
. . . . 5
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β ((πΉβπ)(ballβπ)π
) β π₯ β ((πΉβπ)(ballβπ)π
))) |
65 | 62, 63, 64 | 3bitr3d 309 |
. . . 4
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β§ π₯ β π) β (π₯ β (πΉ β (π(ballβπ)π
)) β π₯ β ((πΉβπ)(ballβπ)π
))) |
66 | 65 | ex 412 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (π₯ β π β (π₯ β (πΉ β (π(ballβπ)π
)) β π₯ β ((πΉβπ)(ballβπ)π
)))) |
67 | 10, 18, 66 | pm5.21ndd 379 |
. 2
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (π₯ β (πΉ β (π(ballβπ)π
)) β π₯ β ((πΉβπ)(ballβπ)π
))) |
68 | 67 | eqrdv 2724 |
1
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π β π β§ π
β β*)) β (πΉ β (π(ballβπ)π
)) = ((πΉβπ)(ballβπ)π
)) |