Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ ((π½ β π΄ β§ π β π) β π½ β π΄) |
2 | | f1oi 6826 |
. . 3
β’ ( I
βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1-ontoβ(π β© βͺ π½) |
3 | | f1of1 6787 |
. . 3
β’ (( I
βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1-ontoβ(π β© βͺ π½) β ( I βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1β(π β© βͺ π½)) |
4 | 2, 3 | mp1i 13 |
. 2
β’ ((π½ β π΄ β§ π β π) β ( I βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1β(π β© βͺ π½)) |
5 | | inss2 4193 |
. . . . 5
β’ (π β© βͺ π½)
β βͺ π½ |
6 | | resabs1 5971 |
. . . . 5
β’ ((π β© βͺ π½)
β βͺ π½ β (( I βΎ βͺ π½)
βΎ (π β© βͺ π½))
= ( I βΎ (π β©
βͺ π½))) |
7 | 5, 6 | ax-mp 5 |
. . . 4
β’ (( I
βΎ βͺ π½) βΎ (π β© βͺ π½)) = ( I βΎ (π β© βͺ π½)) |
8 | | resthauslem.1 |
. . . . . . . 8
β’ (π½ β π΄ β π½ β Top) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π½ β π΄ β§ π β π) β π½ β Top) |
10 | | toptopon2 22290 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
11 | 9, 10 | sylib 217 |
. . . . . 6
β’ ((π½ β π΄ β§ π β π) β π½ β (TopOnββͺ π½)) |
12 | | idcn 22631 |
. . . . . 6
β’ (π½ β (TopOnββͺ π½)
β ( I βΎ βͺ π½) β (π½ Cn π½)) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ ((π½ β π΄ β§ π β π) β ( I βΎ βͺ π½)
β (π½ Cn π½)) |
14 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
15 | 14 | cnrest 22659 |
. . . . 5
β’ ((( I
βΎ βͺ π½) β (π½ Cn π½) β§ (π β© βͺ π½) β βͺ π½)
β (( I βΎ βͺ π½) βΎ (π β© βͺ π½)) β ((π½ βΎt (π β© βͺ π½)) Cn π½)) |
16 | 13, 5, 15 | sylancl 587 |
. . . 4
β’ ((π½ β π΄ β§ π β π) β (( I βΎ βͺ π½)
βΎ (π β© βͺ π½))
β ((π½
βΎt (π
β© βͺ π½)) Cn π½)) |
17 | 7, 16 | eqeltrrid 2839 |
. . 3
β’ ((π½ β π΄ β§ π β π) β ( I βΎ (π β© βͺ π½)) β ((π½ βΎt (π β© βͺ π½)) Cn π½)) |
18 | 14 | restin 22540 |
. . . 4
β’ ((π½ β π΄ β§ π β π) β (π½ βΎt π) = (π½ βΎt (π β© βͺ π½))) |
19 | 18 | oveq1d 7376 |
. . 3
β’ ((π½ β π΄ β§ π β π) β ((π½ βΎt π) Cn π½) = ((π½ βΎt (π β© βͺ π½)) Cn π½)) |
20 | 17, 19 | eleqtrrd 2837 |
. 2
β’ ((π½ β π΄ β§ π β π) β ( I βΎ (π β© βͺ π½)) β ((π½ βΎt π) Cn π½)) |
21 | | resthauslem.2 |
. 2
β’ ((π½ β π΄ β§ ( I βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1β(π β© βͺ π½) β§ ( I βΎ (π β© βͺ π½))
β ((π½
βΎt π) Cn
π½)) β (π½ βΎt π) β π΄) |
22 | 1, 4, 20, 21 | syl3anc 1372 |
1
β’ ((π½ β π΄ β§ π β π) β (π½ βΎt π) β π΄) |