Step | Hyp | Ref
| Expression |
1 | | isismty 36669 |
. . . . . . . . . . . . 13
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ§ β π βπ€ β π (π§ππ€) = ((πΉβπ§)π(πΉβπ€))))) |
2 | 1 | biimp3a 1470 |
. . . . . . . . . . . 12
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β (πΉ:πβ1-1-ontoβπ β§ βπ§ β π βπ€ β π (π§ππ€) = ((πΉβπ§)π(πΉβπ€)))) |
3 | 2 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β πΉ:πβ1-1-ontoβπ) |
4 | | f1ocnv 6846 |
. . . . . . . . . . 11
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
5 | | f1of 6834 |
. . . . . . . . . . 11
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β β‘πΉ:πβΆπ) |
7 | 6 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π¦ β π) β (β‘πΉβπ¦) β π) |
8 | | oveq1 7416 |
. . . . . . . . . . . 12
β’ (π₯ = (β‘πΉβπ¦) β (π₯(ballβπ)π) = ((β‘πΉβπ¦)(ballβπ)π)) |
9 | 8 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π₯ = (β‘πΉβπ¦) β (π = (π₯(ballβπ)π) β π = ((β‘πΉβπ¦)(ballβπ)π))) |
10 | 9 | rexbidv 3179 |
. . . . . . . . . 10
β’ (π₯ = (β‘πΉβπ¦) β (βπ β β+ π = (π₯(ballβπ)π) β βπ β β+ π = ((β‘πΉβπ¦)(ballβπ)π))) |
11 | 10 | rspcv 3609 |
. . . . . . . . 9
β’ ((β‘πΉβπ¦) β π β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ β β+ π = ((β‘πΉβπ¦)(ballβπ)π))) |
12 | 7, 11 | syl 17 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π¦ β π) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ β β+ π = ((β‘πΉβπ¦)(ballβπ)π))) |
13 | | imaeq2 6056 |
. . . . . . . . . . 11
β’ (π = ((β‘πΉβπ¦)(ballβπ)π) β (πΉ β π) = (πΉ β ((β‘πΉβπ¦)(ballβπ)π))) |
14 | | f1ofo 6841 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβontoβπ) |
15 | | foima 6811 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβontoβπ β (πΉ β π) = π) |
16 | 3, 14, 15 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β (πΉ β π) = π) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β (πΉ β π) = π) |
18 | | rpxr 12983 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β π β
β*) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π β β+) β π β
β*) |
20 | 7, 19 | anim12dan 620 |
. . . . . . . . . . . . . 14
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β ((β‘πΉβπ¦) β π β§ π β
β*)) |
21 | | ismtyima 36671 |
. . . . . . . . . . . . . 14
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ ((β‘πΉβπ¦) β π β§ π β β*)) β (πΉ β ((β‘πΉβπ¦)(ballβπ)π)) = ((πΉβ(β‘πΉβπ¦))(ballβπ)π)) |
22 | 20, 21 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β (πΉ β ((β‘πΉβπ¦)(ballβπ)π)) = ((πΉβ(β‘πΉβπ¦))(ballβπ)π)) |
23 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π β§ π β β+) β π¦ β π) |
24 | | f1ocnvfv2 7275 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:πβ1-1-ontoβπ β§ π¦ β π) β (πΉβ(β‘πΉβπ¦)) = π¦) |
25 | 3, 23, 24 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β (πΉβ(β‘πΉβπ¦)) = π¦) |
26 | 25 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β ((πΉβ(β‘πΉβπ¦))(ballβπ)π) = (π¦(ballβπ)π)) |
27 | 22, 26 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β (πΉ β ((β‘πΉβπ¦)(ballβπ)π)) = (π¦(ballβπ)π)) |
28 | 17, 27 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β ((πΉ β π) = (πΉ β ((β‘πΉβπ¦)(ballβπ)π)) β π = (π¦(ballβπ)π))) |
29 | 13, 28 | imbitrid 243 |
. . . . . . . . . 10
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ (π¦ β π β§ π β β+)) β (π = ((β‘πΉβπ¦)(ballβπ)π) β π = (π¦(ballβπ)π))) |
30 | 29 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π¦ β π) β§ π β β+) β (π = ((β‘πΉβπ¦)(ballβπ)π) β π = (π¦(ballβπ)π))) |
31 | 30 | reximdva 3169 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π¦ β π) β (βπ β β+ π = ((β‘πΉβπ¦)(ballβπ)π) β βπ β β+ π = (π¦(ballβπ)π))) |
32 | 12, 31 | syld 47 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β§ π¦ β π) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ β β+ π = (π¦(ballβπ)π))) |
33 | 32 | ralrimdva 3155 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
34 | | simp2 1138 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β π β (βMetβπ)) |
35 | 33, 34 | jctild 527 |
. . . . 5
β’ ((π β (βMetβπ) β§ π β (βMetβπ) β§ πΉ β (π Ismty π)) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)))) |
36 | 35 | 3expib 1123 |
. . . 4
β’ (π β (βMetβπ) β ((π β (βMetβπ) β§ πΉ β (π Ismty π)) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))))) |
37 | 36 | com12 32 |
. . 3
β’ ((π β (βMetβπ) β§ πΉ β (π Ismty π)) β (π β (βMetβπ) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))))) |
38 | 37 | impd 412 |
. 2
β’ ((π β (βMetβπ) β§ πΉ β (π Ismty π)) β ((π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)))) |
39 | | isbndx 36650 |
. 2
β’ (π β (Bndβπ) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
40 | | isbndx 36650 |
. 2
β’ (π β (Bndβπ) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
41 | 38, 39, 40 | 3imtr4g 296 |
1
β’ ((π β (βMetβπ) β§ πΉ β (π Ismty π)) β (π β (Bndβπ) β π β (Bndβπ))) |