Step | Hyp | Ref
| Expression |
1 | | toponss 22773 |
. . . . 5
β’ ((πΎ β (TopOnβπ) β§ π₯ β πΎ) β π₯ β π) |
2 | 1 | 3ad2antl2 1183 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π₯ β π) |
3 | | cnima 23113 |
. . . . 5
β’ ((πΉ β (π½ Cn πΎ) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
4 | 3 | 3ad2antl1 1182 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
5 | | simpl1 1188 |
. . . . . . 7
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ β (π½ Cn πΎ)) |
6 | | cntop1 23088 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π½ β Top) |
8 | | toptopon2 22764 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π½ β (TopOnββͺ π½)) |
10 | | simpl2 1189 |
. . . . . . . 8
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΎ β (TopOnβπ)) |
11 | | cnf2 23097 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆπ) |
12 | 9, 10, 5, 11 | syl3anc 1368 |
. . . . . . 7
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ:βͺ π½βΆπ) |
13 | 12 | ffnd 6709 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ Fn βͺ π½) |
14 | | simpl3 1190 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β ran πΉ = π) |
15 | | df-fo 6540 |
. . . . . 6
β’ (πΉ:βͺ
π½βontoβπ β (πΉ Fn βͺ π½ β§ ran πΉ = π)) |
16 | 13, 14, 15 | sylanbrc 582 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β πΉ:βͺ π½βontoβπ) |
17 | | elqtop3 23551 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ:βͺ π½βontoβπ) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
18 | 9, 16, 17 | syl2anc 583 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
19 | 2, 4, 18 | mpbir2and 710 |
. . 3
β’ (((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β§ π₯ β πΎ) β π₯ β (π½ qTop πΉ)) |
20 | 19 | ex 412 |
. 2
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β (π₯ β πΎ β π₯ β (π½ qTop πΉ))) |
21 | 20 | ssrdv 3981 |
1
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) |