Step | Hyp | Ref
| Expression |
1 | | toponss 22299 |
. . . . 5
β’ ((πΎ β (TopOnβπ) β§ π₯ β πΎ) β π₯ β π) |
2 | 1 | 3ad2antl2 1187 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π₯ β π) |
3 | | cnima 22639 |
. . . . 5
β’ ((πΉ β (π½ Cn πΎ) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
4 | 3 | 3ad2antl1 1186 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
5 | | simpl1 1192 |
. . . . . . 7
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ β (π½ Cn πΎ)) |
6 | | cntop1 22614 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π½ β Top) |
8 | | toptopon2 22290 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π½ β (TopOnββͺ π½)) |
10 | | simpl2 1193 |
. . . . . . . 8
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΎ β (TopOnβπ)) |
11 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆπ) |
12 | 9, 10, 5, 11 | syl3anc 1372 |
. . . . . . 7
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ:βͺ π½βΆπ) |
13 | 12 | ffnd 6673 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ Fn βͺ π½) |
14 | | simpl3 1194 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β ran πΉ = π) |
15 | | df-fo 6506 |
. . . . . 6
β’ (πΉ:βͺ
π½βontoβπ β (πΉ Fn βͺ π½ β§ ran πΉ = π)) |
16 | 13, 14, 15 | sylanbrc 584 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ:βͺ π½βontoβπ) |
17 | | elqtop3 23077 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ:βͺ π½βontoβπ) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
18 | 9, 16, 17 | syl2anc 585 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
19 | 2, 4, 18 | mpbir2and 712 |
. . 3
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π₯ β (π½ qTop πΉ)) |
20 | 19 | ex 414 |
. 2
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β (π₯ β πΎ β π₯ β (π½ qTop πΉ))) |
21 | 20 | ssrdv 3954 |
1
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) |