Step | Hyp | Ref
| Expression |
1 | | nfcv 2899 |
. . 3
β’
β²ππΆ |
2 | | nfcsb1v 3919 |
. . 3
β’
β²πβ¦π / πβ¦πΆ |
3 | | csbeq1a 3908 |
. . 3
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
4 | 1, 2, 3 | cbvixp 8941 |
. 2
β’ Xπ β
π΄ πΆ = Xπ β π΄ β¦π / πβ¦πΆ |
5 | | ptcldmpt.a |
. . 3
β’ (π β π΄ β π) |
6 | | ptcldmpt.j |
. . . 4
β’ ((π β§ π β π΄) β π½ β Top) |
7 | 6 | fmpttd 7130 |
. . 3
β’ (π β (π β π΄ β¦ π½):π΄βΆTop) |
8 | | nfv 1909 |
. . . . 5
β’
β²π(π β§ π β π΄) |
9 | | nfcv 2899 |
. . . . . . 7
β’
β²πClsd |
10 | | nffvmpt1 6913 |
. . . . . . 7
β’
β²π((π β π΄ β¦ π½)βπ) |
11 | 9, 10 | nffv 6912 |
. . . . . 6
β’
β²π(Clsdβ((π β π΄ β¦ π½)βπ)) |
12 | 2, 11 | nfel 2914 |
. . . . 5
β’
β²πβ¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)) |
13 | 8, 12 | nfim 1891 |
. . . 4
β’
β²π((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
14 | | eleq1w 2812 |
. . . . . 6
β’ (π = π β (π β π΄ β π β π΄)) |
15 | 14 | anbi2d 628 |
. . . . 5
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
16 | | 2fveq3 6907 |
. . . . . 6
β’ (π = π β (Clsdβ((π β π΄ β¦ π½)βπ)) = (Clsdβ((π β π΄ β¦ π½)βπ))) |
17 | 3, 16 | eleq12d 2823 |
. . . . 5
β’ (π = π β (πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)))) |
18 | 15, 17 | imbi12d 343 |
. . . 4
β’ (π = π β (((π β§ π β π΄) β πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) β ((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))))) |
19 | | ptcldmpt.c |
. . . . 5
β’ ((π β§ π β π΄) β πΆ β (Clsdβπ½)) |
20 | | simpr 483 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β π΄) |
21 | | eqid 2728 |
. . . . . . . 8
β’ (π β π΄ β¦ π½) = (π β π΄ β¦ π½) |
22 | 21 | fvmpt2 7021 |
. . . . . . 7
β’ ((π β π΄ β§ π½ β Top) β ((π β π΄ β¦ π½)βπ) = π½) |
23 | 20, 6, 22 | syl2anc 582 |
. . . . . 6
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π½)βπ) = π½) |
24 | 23 | fveq2d 6906 |
. . . . 5
β’ ((π β§ π β π΄) β (Clsdβ((π β π΄ β¦ π½)βπ)) = (Clsdβπ½)) |
25 | 19, 24 | eleqtrrd 2832 |
. . . 4
β’ ((π β§ π β π΄) β πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
26 | 13, 18, 25 | chvarfv 2228 |
. . 3
β’ ((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
27 | 5, 7, 26 | ptcld 23545 |
. 2
β’ (π β Xπ β
π΄ β¦π / πβ¦πΆ β
(Clsdβ(βtβ(π β π΄ β¦ π½)))) |
28 | 4, 27 | eqeltrid 2833 |
1
β’ (π β Xπ β
π΄ πΆ β
(Clsdβ(βtβ(π β π΄ β¦ π½)))) |