Step | Hyp | Ref
| Expression |
1 | | qtopt1.1 |
. . . 4
β’ (π β π½ β Fre) |
2 | | t1top 23184 |
. . . 4
β’ (π½ β Fre β π½ β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π½ β Top) |
4 | | qtopt1.2 |
. . . 4
β’ (π β πΉ:πβontoβπ) |
5 | | fofn 6800 |
. . . 4
β’ (πΉ:πβontoβπ β πΉ Fn π) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β πΉ Fn π) |
7 | | qtopt1.x |
. . . 4
β’ π = βͺ
π½ |
8 | 7 | qtoptop 23554 |
. . 3
β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) |
9 | 3, 6, 8 | syl2anc 583 |
. 2
β’ (π β (π½ qTop πΉ) β Top) |
10 | | simpr 484 |
. . . . . 6
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π₯ β βͺ (π½ qTop πΉ)) |
11 | 7 | qtopuni 23556 |
. . . . . . . 8
β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) |
12 | 3, 4, 11 | syl2anc 583 |
. . . . . . 7
β’ (π β π = βͺ (π½ qTop πΉ)) |
13 | 12 | adantr 480 |
. . . . . 6
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π = βͺ (π½ qTop πΉ)) |
14 | 10, 13 | eleqtrrd 2830 |
. . . . 5
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β π₯ β π) |
15 | 14 | snssd 4807 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β {π₯} β π) |
16 | | qtopt1.3 |
. . . . 5
β’ ((π β§ π₯ β π) β (β‘πΉ β {π₯}) β (Clsdβπ½)) |
17 | 14, 16 | syldan 590 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β (β‘πΉ β {π₯}) β (Clsdβπ½)) |
18 | 3, 7 | jctir 520 |
. . . . . . 7
β’ (π β (π½ β Top β§ π = βͺ π½)) |
19 | | istopon 22764 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
20 | 18, 19 | sylibr 233 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
21 | | qtopcld 23567 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
22 | 20, 4, 21 | syl2anc 583 |
. . . . 5
β’ (π β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
23 | 22 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β ({π₯} β (Clsdβ(π½ qTop πΉ)) β ({π₯} β π β§ (β‘πΉ β {π₯}) β (Clsdβπ½)))) |
24 | 15, 17, 23 | mpbir2and 710 |
. . 3
β’ ((π β§ π₯ β βͺ (π½ qTop πΉ)) β {π₯} β (Clsdβ(π½ qTop πΉ))) |
25 | 24 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β βͺ (π½ qTop πΉ){π₯} β (Clsdβ(π½ qTop πΉ))) |
26 | | eqid 2726 |
. . 3
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
27 | 26 | ist1 23175 |
. 2
β’ ((π½ qTop πΉ) β Fre β ((π½ qTop πΉ) β Top β§ βπ₯ β βͺ (π½
qTop πΉ){π₯} β (Clsdβ(π½ qTop πΉ)))) |
28 | 9, 25, 27 | sylanbrc 582 |
1
β’ (π β (π½ qTop πΉ) β Fre) |