Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . 5
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π΄ β (π½ fClus πΉ)) |
2 | | fclstop 23735 |
. . . . 5
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) |
3 | 1, 2 | syl 17 |
. . . 4
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π½ β Top) |
4 | | simp2 1137 |
. . . . 5
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π β ((neiβπ½)β{π΄})) |
5 | | eqid 2732 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
6 | 5 | neii1 22830 |
. . . . 5
β’ ((π½ β Top β§ π β ((neiβπ½)β{π΄})) β π β βͺ π½) |
7 | 3, 4, 6 | syl2anc 584 |
. . . 4
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π β βͺ π½) |
8 | 5 | ntrss2 22781 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
9 | 3, 7, 8 | syl2anc 584 |
. . 3
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β ((intβπ½)βπ) β π) |
10 | 9 | ssrind 4235 |
. 2
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (((intβπ½)βπ) β© π) β (π β© π)) |
11 | 5 | ntropn 22773 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π½) |
12 | 3, 7, 11 | syl2anc 584 |
. . 3
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β ((intβπ½)βπ) β π½) |
13 | 5 | fclselbas 23740 |
. . . . . . . 8
β’ (π΄ β (π½ fClus πΉ) β π΄ β βͺ π½) |
14 | 1, 13 | syl 17 |
. . . . . . 7
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π΄ β βͺ π½) |
15 | 14 | snssd 4812 |
. . . . . 6
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β {π΄} β βͺ π½) |
16 | 5 | neiint 22828 |
. . . . . 6
β’ ((π½ β Top β§ {π΄} β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
17 | 3, 15, 7, 16 | syl3anc 1371 |
. . . . 5
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (π β ((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
18 | 4, 17 | mpbid 231 |
. . . 4
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β {π΄} β ((intβπ½)βπ)) |
19 | | snssg 4787 |
. . . . 5
β’ (π΄ β βͺ π½
β (π΄ β
((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
20 | 14, 19 | syl 17 |
. . . 4
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (π΄ β ((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
21 | 18, 20 | mpbird 256 |
. . 3
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π΄ β ((intβπ½)βπ)) |
22 | | simp3 1138 |
. . 3
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β π β πΉ) |
23 | | fclsopni 23739 |
. . 3
β’ ((π΄ β (π½ fClus πΉ) β§ (((intβπ½)βπ) β π½ β§ π΄ β ((intβπ½)βπ) β§ π β πΉ)) β (((intβπ½)βπ) β© π) β β
) |
24 | 1, 12, 21, 22, 23 | syl13anc 1372 |
. 2
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (((intβπ½)βπ) β© π) β β
) |
25 | | ssn0 4400 |
. 2
β’
(((((intβπ½)βπ) β© π) β (π β© π) β§ (((intβπ½)βπ) β© π) β β
) β (π β© π) β β
) |
26 | 10, 24, 25 | syl2anc 584 |
1
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (π β© π) β β
) |