Step | Hyp | Ref
| Expression |
1 | | topontop 22285 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | 1 | 3ad2ant1 1134 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β π½ β Top) |
3 | | elpwi 4571 |
. . . 4
β’ (π₯ β π« π½ β π₯ β π½) |
4 | | simpl2 1193 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β πΎ β Comp) |
5 | | simprl 770 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π₯ β π½) |
6 | | simpl3 1194 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π½ β πΎ) |
7 | 5, 6 | sstrd 3958 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π₯ β πΎ) |
8 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π½ β (TopOnβπ)) |
9 | | toponuni 22286 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π = βͺ
π½) |
11 | | simprr 772 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β βͺ π½ =
βͺ π₯) |
12 | 10, 11 | eqtrd 2773 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β π = βͺ
π₯) |
13 | | sscmp.1 |
. . . . . . . 8
β’ π = βͺ
πΎ |
14 | 13 | cmpcov 22763 |
. . . . . . 7
β’ ((πΎ β Comp β§ π₯ β πΎ β§ π = βͺ π₯) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) |
15 | 4, 7, 12, 14 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) |
16 | 10 | eqeq1d 2735 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β (π = βͺ
π¦ β βͺ π½ =
βͺ π¦)) |
17 | 16 | rexbidv 3172 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β (βπ¦ β (π« π₯ β© Fin)π = βͺ π¦ β βπ¦ β (π« π₯ β© Fin)βͺ π½ =
βͺ π¦)) |
18 | 15, 17 | mpbid 231 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ (π₯ β π½ β§ βͺ π½ = βͺ
π₯)) β βπ¦ β (π« π₯ β© Fin)βͺ π½ =
βͺ π¦) |
19 | 18 | expr 458 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ π₯ β π½) β (βͺ π½ = βͺ
π₯ β βπ¦ β (π« π₯ β© Fin)βͺ π½ =
βͺ π¦)) |
20 | 3, 19 | sylan2 594 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β§ π₯ β π« π½) β (βͺ π½ = βͺ
π₯ β βπ¦ β (π« π₯ β© Fin)βͺ π½ =
βͺ π¦)) |
21 | 20 | ralrimiva 3140 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β βπ₯ β π« π½(βͺ π½ = βͺ
π₯ β βπ¦ β (π« π₯ β© Fin)βͺ π½ =
βͺ π¦)) |
22 | | eqid 2733 |
. . 3
β’ βͺ π½ =
βͺ π½ |
23 | 22 | iscmp 22762 |
. 2
β’ (π½ β Comp β (π½ β Top β§ βπ₯ β π« π½(βͺ
π½ = βͺ π₯
β βπ¦ β
(π« π₯ β©
Fin)βͺ π½ = βͺ π¦))) |
24 | 2, 21, 23 | sylanbrc 584 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β π½ β Comp) |