Step | Hyp | Ref
| Expression |
1 | | resttopon 22535 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) |
2 | | dfconn2 22793 |
. . 3
β’ ((π½ βΎt π΄) β (TopOnβπ΄) β ((π½ βΎt π΄) β Conn β βπ’ β (π½ βΎt π΄)βπ£ β (π½ βΎt π΄)((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β (π’ βͺ π£) β π΄))) |
3 | 1, 2 | syl 17 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((π½ βΎt π΄) β Conn β βπ’ β (π½ βΎt π΄)βπ£ β (π½ βΎt π΄)((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β (π’ βͺ π£) β π΄))) |
4 | | vex 3451 |
. . . . 5
β’ π₯ β V |
5 | 4 | inex1 5278 |
. . . 4
β’ (π₯ β© π΄) β V |
6 | 5 | a1i 11 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π₯ β π½) β (π₯ β© π΄) β V) |
7 | | toponmax 22298 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β π½) |
9 | | simpr 486 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) |
10 | 8, 9 | ssexd 5285 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β V) |
11 | | elrest 17317 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β V) β (π’ β (π½ βΎt π΄) β βπ₯ β π½ π’ = (π₯ β© π΄))) |
12 | 10, 11 | syldan 592 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π’ β (π½ βΎt π΄) β βπ₯ β π½ π’ = (π₯ β© π΄))) |
13 | | vex 3451 |
. . . . . 6
β’ π¦ β V |
14 | 13 | inex1 5278 |
. . . . 5
β’ (π¦ β© π΄) β V |
15 | 14 | a1i 11 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π¦ β π½) β (π¦ β© π΄) β V) |
16 | | elrest 17317 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β V) β (π£ β (π½ βΎt π΄) β βπ¦ β π½ π£ = (π¦ β© π΄))) |
17 | 10, 16 | syldan 592 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π£ β (π½ βΎt π΄) β βπ¦ β π½ π£ = (π¦ β© π΄))) |
18 | 17 | adantr 482 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β (π£ β (π½ βΎt π΄) β βπ¦ β π½ π£ = (π¦ β© π΄))) |
19 | | simplr 768 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β π’ = (π₯ β© π΄)) |
20 | 19 | neeq1d 3000 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π’ β β
β (π₯ β© π΄) β β
)) |
21 | | simpr 486 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β π£ = (π¦ β© π΄)) |
22 | 21 | neeq1d 3000 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π£ β β
β (π¦ β© π΄) β β
)) |
23 | 19, 21 | ineq12d 4177 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π’ β© π£) = ((π₯ β© π΄) β© (π¦ β© π΄))) |
24 | | inindir 4191 |
. . . . . . . 8
β’ ((π₯ β© π¦) β© π΄) = ((π₯ β© π΄) β© (π¦ β© π΄)) |
25 | 23, 24 | eqtr4di 2791 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π’ β© π£) = ((π₯ β© π¦) β© π΄)) |
26 | 25 | eqeq1d 2735 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β ((π’ β© π£) = β
β ((π₯ β© π¦) β© π΄) = β
)) |
27 | 20, 22, 26 | 3anbi123d 1437 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β ((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β ((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
))) |
28 | 19, 21 | uneq12d 4128 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π’ βͺ π£) = ((π₯ β© π΄) βͺ (π¦ β© π΄))) |
29 | | indir 4239 |
. . . . . . 7
β’ ((π₯ βͺ π¦) β© π΄) = ((π₯ β© π΄) βͺ (π¦ β© π΄)) |
30 | 28, 29 | eqtr4di 2791 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (π’ βͺ π£) = ((π₯ βͺ π¦) β© π΄)) |
31 | 30 | neeq1d 3000 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β ((π’ βͺ π£) β π΄ β ((π₯ βͺ π¦) β© π΄) β π΄)) |
32 | 27, 31 | imbi12d 345 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β§ π£ = (π¦ β© π΄)) β (((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β (π’ βͺ π£) β π΄) β (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |
33 | 15, 18, 32 | ralxfr2d 5369 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π’ = (π₯ β© π΄)) β (βπ£ β (π½ βΎt π΄)((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β (π’ βͺ π£) β π΄) β βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |
34 | 6, 12, 33 | ralxfr2d 5369 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (βπ’ β (π½ βΎt π΄)βπ£ β (π½ βΎt π΄)((π’ β β
β§ π£ β β
β§ (π’ β© π£) = β
) β (π’ βͺ π£) β π΄) β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |
35 | 3, 34 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((π½ βΎt π΄) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |