Step | Hyp | Ref
| Expression |
1 | | disjdif 4435 |
. . . . 5
β’
(((intβπ½)βπ΄) β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
|
2 | 1 | a1i 11 |
. . . 4
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)βπ΄) β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
) |
3 | | ineq1 4169 |
. . . . 5
β’
(((intβπ½)βπ΄) = π΄ β (((intβπ½)βπ΄) β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄)))) |
4 | 3 | eqeq1d 2735 |
. . . 4
β’
(((intβπ½)βπ΄) = π΄ β ((((intβπ½)βπ΄) β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
β (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
)) |
5 | 2, 4 | syl5ibcom 244 |
. . 3
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)βπ΄) = π΄ β (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
)) |
6 | | opnbnd.1 |
. . . . . . 7
β’ π = βͺ
π½ |
7 | 6 | ntrss2 22431 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β π) β ((intβπ½)βπ΄) β π΄) |
8 | 7 | adantr 482 |
. . . . 5
β’ (((π½ β Top β§ π΄ β π) β§ (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
) β ((intβπ½)βπ΄) β π΄) |
9 | | inssdif0 4333 |
. . . . . 6
β’ ((π΄ β© ((clsβπ½)βπ΄)) β ((intβπ½)βπ΄) β (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
) |
10 | 6 | sscls 22430 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π΄ β π) β π΄ β ((clsβπ½)βπ΄)) |
11 | | df-ss 3931 |
. . . . . . . . . 10
β’ (π΄ β ((clsβπ½)βπ΄) β (π΄ β© ((clsβπ½)βπ΄)) = π΄) |
12 | 10, 11 | sylib 217 |
. . . . . . . . 9
β’ ((π½ β Top β§ π΄ β π) β (π΄ β© ((clsβπ½)βπ΄)) = π΄) |
13 | 12 | eqcomd 2739 |
. . . . . . . 8
β’ ((π½ β Top β§ π΄ β π) β π΄ = (π΄ β© ((clsβπ½)βπ΄))) |
14 | | eqimss 4004 |
. . . . . . . 8
β’ (π΄ = (π΄ β© ((clsβπ½)βπ΄)) β π΄ β (π΄ β© ((clsβπ½)βπ΄))) |
15 | 13, 14 | syl 17 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β π΄ β (π΄ β© ((clsβπ½)βπ΄))) |
16 | | sstr 3956 |
. . . . . . 7
β’ ((π΄ β (π΄ β© ((clsβπ½)βπ΄)) β§ (π΄ β© ((clsβπ½)βπ΄)) β ((intβπ½)βπ΄)) β π΄ β ((intβπ½)βπ΄)) |
17 | 15, 16 | sylan 581 |
. . . . . 6
β’ (((π½ β Top β§ π΄ β π) β§ (π΄ β© ((clsβπ½)βπ΄)) β ((intβπ½)βπ΄)) β π΄ β ((intβπ½)βπ΄)) |
18 | 9, 17 | sylan2br 596 |
. . . . 5
β’ (((π½ β Top β§ π΄ β π) β§ (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
) β π΄ β ((intβπ½)βπ΄)) |
19 | 8, 18 | eqssd 3965 |
. . . 4
β’ (((π½ β Top β§ π΄ β π) β§ (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
) β ((intβπ½)βπ΄) = π΄) |
20 | 19 | ex 414 |
. . 3
β’ ((π½ β Top β§ π΄ β π) β ((π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
β ((intβπ½)βπ΄) = π΄)) |
21 | 5, 20 | impbid 211 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)βπ΄) = π΄ β (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
)) |
22 | 6 | isopn3 22440 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β ((intβπ½)βπ΄) = π΄)) |
23 | 6 | topbnd 34849 |
. . . 4
β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) |
24 | 23 | ineq2d 4176 |
. . 3
β’ ((π½ β Top β§ π΄ β π) β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄)))) |
25 | 24 | eqeq1d 2735 |
. 2
β’ ((π½ β Top β§ π΄ β π) β ((π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β
β (π΄ β© (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) = β
)) |
26 | 21, 22, 25 | 3bitr4d 311 |
1
β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β
)) |