Step | Hyp | Ref
| Expression |
1 | | qtopt1.1 |
. . . 4
β’ (π β π½ β Fre) |
2 | | t1top 22825 |
. . . 4
β’ (π½ β Fre β π½ β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π½ β Top) |
4 | | qtopt1.2 |
. . . 4
β’ (π β πΉ:πβontoβπ) |
5 | | fofn 6804 |
. . . 4
β’ (πΉ:πβontoβπ β πΉ Fn π) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β πΉ Fn π) |
7 | | qtopt1.x |
. . . 4
β’ π = βͺ
π½ |
8 | 7 | qtoptop 23195 |
. . 3
β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) |
9 | 3, 6, 8 | syl2anc 584 |
. 2
β’ (π β (π½ qTop πΉ) β Top) |
10 | | simpr 485 |
. . . . . 6
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π₯ β βͺ (π½ qTop πΉ)) |
11 | 7 | qtopuni 23197 |
. . . . . . . 8
β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) |
12 | 3, 4, 11 | syl2anc 584 |
. . . . . . 7
β’ (π β π = βͺ (π½ qTop πΉ)) |
13 | 12 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π = βͺ (π½ qTop πΉ)) |
14 | 10, 13 | eleqtrrd 2836 |
. . . . 5
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π₯ β π) |
15 | 14 | snssd 4811 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β {π₯} β π) |
16 | | qtopt1.3 |
. . . . 5
β’ ((π β§ π₯ β π) β (β‘πΉ β {π₯}) β (Clsdβπ½)) |
17 | 14, 16 | syldan 591 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β (β‘πΉ β {π₯}) β (Clsdβπ½)) |
18 | 3, 7 | jctir 521 |
. . . . . . 7
β’ (π β (π½ β Top β§ π = βͺ π½)) |
19 | | istopon 22405 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
20 | 18, 19 | sylibr 233 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
21 | | qtopcld 23208 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
22 | 20, 4, 21 | syl2anc 584 |
. . . . 5
β’ (π β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
23 | 22 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
24 | 15, 17, 23 | mpbir2and 711 |
. . 3
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β {π₯} β (Clsdβ(π½ qTop πΉ))) |
25 | 24 | ralrimiva 3146 |
. 2
β’ (π β βπ₯ β βͺ (π½ qTop πΉ){π₯} β (Clsdβ(π½ qTop πΉ))) |
26 | | eqid 2732 |
. . 3
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
27 | 26 | ist1 22816 |
. 2
β’ ((π½ qTop πΉ) β Fre β ((π½ qTop πΉ) β Top β§ βπ₯ β βͺ (π½
qTop πΉ){π₯} β (Clsdβ(π½ qTop πΉ)))) |
28 | 9, 25, 27 | sylanbrc 583 |
1
β’ (π β (π½ qTop πΉ) β Fre) |