Step | Hyp | Ref
| Expression |
1 | | nfcv 2897 |
. . 3
β’
β²ππΆ |
2 | | nfcsb1v 3913 |
. . 3
β’
β²πβ¦π / πβ¦πΆ |
3 | | csbeq1a 3902 |
. . 3
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
4 | 1, 2, 3 | cbvixp 8910 |
. 2
β’ Xπ β
π΄ πΆ = Xπ β π΄ β¦π / πβ¦πΆ |
5 | | ptcldmpt.a |
. . 3
β’ (π β π΄ β π) |
6 | | ptcldmpt.j |
. . . 4
β’ ((π β§ π β π΄) β π½ β Top) |
7 | 6 | fmpttd 7110 |
. . 3
β’ (π β (π β π΄ β¦ π½):π΄βΆTop) |
8 | | nfv 1909 |
. . . . 5
β’
β²π(π β§ π β π΄) |
9 | | nfcv 2897 |
. . . . . . 7
β’
β²πClsd |
10 | | nffvmpt1 6896 |
. . . . . . 7
β’
β²π((π β π΄ β¦ π½)βπ) |
11 | 9, 10 | nffv 6895 |
. . . . . 6
β’
β²π(Clsdβ((π β π΄ β¦ π½)βπ)) |
12 | 2, 11 | nfel 2911 |
. . . . 5
β’
β²πβ¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)) |
13 | 8, 12 | nfim 1891 |
. . . 4
β’
β²π((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
14 | | eleq1w 2810 |
. . . . . 6
β’ (π = π β (π β π΄ β π β π΄)) |
15 | 14 | anbi2d 628 |
. . . . 5
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
16 | | 2fveq3 6890 |
. . . . . 6
β’ (π = π β (Clsdβ((π β π΄ β¦ π½)βπ)) = (Clsdβ((π β π΄ β¦ π½)βπ))) |
17 | 3, 16 | eleq12d 2821 |
. . . . 5
β’ (π = π β (πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ)))) |
18 | 15, 17 | imbi12d 344 |
. . . 4
β’ (π = π β (((π β§ π β π΄) β πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) β ((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))))) |
19 | | ptcldmpt.c |
. . . . 5
β’ ((π β§ π β π΄) β πΆ β (Clsdβπ½)) |
20 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β π΄) |
21 | | eqid 2726 |
. . . . . . . 8
β’ (π β π΄ β¦ π½) = (π β π΄ β¦ π½) |
22 | 21 | fvmpt2 7003 |
. . . . . . 7
β’ ((π β π΄ β§ π½ β Top) β ((π β π΄ β¦ π½)βπ) = π½) |
23 | 20, 6, 22 | syl2anc 583 |
. . . . . 6
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π½)βπ) = π½) |
24 | 23 | fveq2d 6889 |
. . . . 5
β’ ((π β§ π β π΄) β (Clsdβ((π β π΄ β¦ π½)βπ)) = (Clsdβπ½)) |
25 | 19, 24 | eleqtrrd 2830 |
. . . 4
β’ ((π β§ π β π΄) β πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
26 | 13, 18, 25 | chvarfv 2225 |
. . 3
β’ ((π β§ π β π΄) β β¦π / πβ¦πΆ β (Clsdβ((π β π΄ β¦ π½)βπ))) |
27 | 5, 7, 26 | ptcld 23472 |
. 2
β’ (π β Xπ β
π΄ β¦π / πβ¦πΆ β
(Clsdβ(βtβ(π β π΄ β¦ π½)))) |
28 | 4, 27 | eqeltrid 2831 |
1
β’ (π β Xπ β
π΄ πΆ β
(Clsdβ(βtβ(π β π΄ β¦ π½)))) |