Step | Hyp | Ref
| Expression |
1 | | cnpfval 22601 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ CnP πΎ) = (π£ β π β¦ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))})) |
2 | 1 | fveq1d 6849 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β ((π½ CnP πΎ)βπ) = ((π£ β π β¦ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))})βπ)) |
3 | | fveq2 6847 |
. . . . . . . 8
β’ (π£ = π β (πβπ£) = (πβπ)) |
4 | 3 | eleq1d 2823 |
. . . . . . 7
β’ (π£ = π β ((πβπ£) β π¦ β (πβπ) β π¦)) |
5 | | eleq1 2826 |
. . . . . . . . 9
β’ (π£ = π β (π£ β π₯ β π β π₯)) |
6 | 5 | anbi1d 631 |
. . . . . . . 8
β’ (π£ = π β ((π£ β π₯ β§ (π β π₯) β π¦) β (π β π₯ β§ (π β π₯) β π¦))) |
7 | 6 | rexbidv 3176 |
. . . . . . 7
β’ (π£ = π β (βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦) β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))) |
8 | 4, 7 | imbi12d 345 |
. . . . . 6
β’ (π£ = π β (((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦)) β ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦)))) |
9 | 8 | ralbidv 3175 |
. . . . 5
β’ (π£ = π β (βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦)) β βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦)))) |
10 | 9 | rabbidv 3418 |
. . . 4
β’ (π£ = π β {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))} = {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) |
11 | | eqid 2737 |
. . . 4
β’ (π£ β π β¦ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))}) = (π£ β π β¦ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))}) |
12 | | ovex 7395 |
. . . . 5
β’ (π βm π) β V |
13 | 12 | rabex 5294 |
. . . 4
β’ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))} β V |
14 | 10, 11, 13 | fvmpt 6953 |
. . 3
β’ (π β π β ((π£ β π β¦ {π β (π βm π) β£ βπ¦ β πΎ ((πβπ£) β π¦ β βπ₯ β π½ (π£ β π₯ β§ (π β π₯) β π¦))})βπ) = {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) |
15 | 2, 14 | sylan9eq 2797 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π β π) β ((π½ CnP πΎ)βπ) = {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) |
16 | 15 | 3impa 1111 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β ((π½ CnP πΎ)βπ) = {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) |