Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
2 | 1 | fclsfil 23377 |
. . . . . . 7
β’ (π΄ β (π½ fClus πΉ) β πΉ β (Filββͺ π½)) |
3 | | fclstopon 23379 |
. . . . . . 7
β’ (π΄ β (π½ fClus πΉ) β (π½ β (TopOnββͺ π½)
β πΉ β
(Filββͺ π½))) |
4 | 2, 3 | mpbird 257 |
. . . . . 6
β’ (π΄ β (π½ fClus πΉ) β π½ β (TopOnββͺ π½)) |
5 | | fclsopn 23381 |
. . . . . 6
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ β
(Filββͺ π½)) β (π΄ β (π½ fClus πΉ) β (π΄ β βͺ π½ β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)))) |
6 | 4, 2, 5 | syl2anc 585 |
. . . . 5
β’ (π΄ β (π½ fClus πΉ) β (π΄ β (π½ fClus πΉ) β (π΄ β βͺ π½ β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)))) |
7 | 6 | ibi 267 |
. . . 4
β’ (π΄ β (π½ fClus πΉ) β (π΄ β βͺ π½ β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
))) |
8 | | eleq2 2827 |
. . . . . 6
β’ (π = π β (π΄ β π β π΄ β π)) |
9 | | ineq1 4170 |
. . . . . . . 8
β’ (π = π β (π β© π ) = (π β© π )) |
10 | 9 | neeq1d 3004 |
. . . . . . 7
β’ (π = π β ((π β© π ) β β
β (π β© π ) β β
)) |
11 | 10 | ralbidv 3175 |
. . . . . 6
β’ (π = π β (βπ β πΉ (π β© π ) β β
β βπ β πΉ (π β© π ) β β
)) |
12 | 8, 11 | imbi12d 345 |
. . . . 5
β’ (π = π β ((π΄ β π β βπ β πΉ (π β© π ) β β
) β (π΄ β π β βπ β πΉ (π β© π ) β β
))) |
13 | 12 | rspccv 3581 |
. . . 4
β’
(βπ β
π½ (π΄ β π β βπ β πΉ (π β© π ) β β
) β (π β π½ β (π΄ β π β βπ β πΉ (π β© π ) β β
))) |
14 | 7, 13 | simpl2im 505 |
. . 3
β’ (π΄ β (π½ fClus πΉ) β (π β π½ β (π΄ β π β βπ β πΉ (π β© π ) β β
))) |
15 | | ineq2 4171 |
. . . . 5
β’ (π = π β (π β© π ) = (π β© π)) |
16 | 15 | neeq1d 3004 |
. . . 4
β’ (π = π β ((π β© π ) β β
β (π β© π) β β
)) |
17 | 16 | rspccv 3581 |
. . 3
β’
(βπ β
πΉ (π β© π ) β β
β (π β πΉ β (π β© π) β β
)) |
18 | 14, 17 | syl8 76 |
. 2
β’ (π΄ β (π½ fClus πΉ) β (π β π½ β (π΄ β π β (π β πΉ β (π β© π) β β
)))) |
19 | 18 | 3imp2 1350 |
1
β’ ((π΄ β (π½ fClus πΉ) β§ (π β π½ β§ π΄ β π β§ π β πΉ)) β (π β© π) β β
) |