Step | Hyp | Ref
| Expression |
1 | | kgentop 22916 |
. . 3
β’ (π½ β ran πGen β
π½ β
Top) |
2 | | qtopcmp.1 |
. . . 4
β’ π = βͺ
π½ |
3 | 2 | qtoptop 23074 |
. . 3
β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) |
4 | 1, 3 | sylan 581 |
. 2
β’ ((π½ β ran πGen β§
πΉ Fn π) β (π½ qTop πΉ) β Top) |
5 | | elssuni 4902 |
. . . . . . . 8
β’ (π₯ β
(πGenβ(π½ qTop
πΉ)) β π₯ β βͺ (πGenβ(π½ qTop πΉ))) |
6 | 5 | adantl 483 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π₯ β βͺ
(πGenβ(π½ qTop
πΉ))) |
7 | 4 | adantr 482 |
. . . . . . . 8
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β (π½ qTop πΉ) β Top) |
8 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
9 | 8 | kgenuni 22913 |
. . . . . . . 8
β’ ((π½ qTop πΉ) β Top β βͺ (π½
qTop πΉ) = βͺ (πGenβ(π½ qTop πΉ))) |
10 | 7, 9 | syl 17 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β βͺ
(π½ qTop πΉ) = βͺ
(πGenβ(π½ qTop
πΉ))) |
11 | 6, 10 | sseqtrrd 3989 |
. . . . . 6
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π₯ β βͺ (π½ qTop πΉ)) |
12 | | simpll 766 |
. . . . . . . 8
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π½ β ran πGen) |
13 | 12, 1 | syl 17 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π½ β Top) |
14 | | simplr 768 |
. . . . . . . 8
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β πΉ Fn π) |
15 | | dffn4 6766 |
. . . . . . . 8
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
16 | 14, 15 | sylib 217 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β πΉ:πβontoβran πΉ) |
17 | 2 | qtopuni 23076 |
. . . . . . 7
β’ ((π½ β Top β§ πΉ:πβontoβran πΉ) β ran πΉ = βͺ (π½ qTop πΉ)) |
18 | 13, 16, 17 | syl2anc 585 |
. . . . . 6
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β ran πΉ = βͺ (π½ qTop πΉ)) |
19 | 11, 18 | sseqtrrd 3989 |
. . . . 5
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π₯ β ran πΉ) |
20 | 2 | toptopon 22289 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnβπ)) |
21 | 13, 20 | sylib 217 |
. . . . . . . 8
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π½ β (TopOnβπ)) |
22 | | qtopid 23079 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) |
23 | 21, 14, 22 | syl2anc 585 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β πΉ β (π½ Cn (π½ qTop πΉ))) |
24 | | kgencn3 22932 |
. . . . . . . 8
β’ ((π½ β ran πGen β§
(π½ qTop πΉ) β Top) β (π½ Cn (π½ qTop πΉ)) = (π½ Cn (πGenβ(π½ qTop πΉ)))) |
25 | 12, 7, 24 | syl2anc 585 |
. . . . . . 7
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β (π½ Cn (π½ qTop πΉ)) = (π½ Cn (πGenβ(π½ qTop πΉ)))) |
26 | 23, 25 | eleqtrd 2836 |
. . . . . 6
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β πΉ β (π½ Cn (πGenβ(π½ qTop πΉ)))) |
27 | | cnima 22639 |
. . . . . 6
β’ ((πΉ β (π½ Cn (πGenβ(π½ qTop πΉ))) β§ π₯ β (πGenβ(π½ qTop πΉ))) β (β‘πΉ β π₯) β π½) |
28 | 26, 27 | sylancom 589 |
. . . . 5
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β (β‘πΉ β π₯) β π½) |
29 | 2 | elqtop2 23075 |
. . . . . 6
β’ ((π½ β ran πGen β§
πΉ:πβontoβran πΉ) β (π₯ β (π½ qTop πΉ) β (π₯ β ran πΉ β§ (β‘πΉ β π₯) β π½))) |
30 | 12, 16, 29 | syl2anc 585 |
. . . . 5
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β (π₯ β (π½ qTop πΉ) β (π₯ β ran πΉ β§ (β‘πΉ β π₯) β π½))) |
31 | 19, 28, 30 | mpbir2and 712 |
. . . 4
β’ (((π½ β ran πGen β§
πΉ Fn π) β§ π₯ β (πGenβ(π½ qTop πΉ))) β π₯ β (π½ qTop πΉ)) |
32 | 31 | ex 414 |
. . 3
β’ ((π½ β ran πGen β§
πΉ Fn π) β (π₯ β (πGenβ(π½ qTop πΉ)) β π₯ β (π½ qTop πΉ))) |
33 | 32 | ssrdv 3954 |
. 2
β’ ((π½ β ran πGen β§
πΉ Fn π) β (πGenβ(π½ qTop πΉ)) β (π½ qTop πΉ)) |
34 | | iskgen2 22922 |
. 2
β’ ((π½ qTop πΉ) β ran πGen β ((π½ qTop πΉ) β Top β§
(πGenβ(π½ qTop
πΉ)) β (π½ qTop πΉ))) |
35 | 4, 33, 34 | sylanbrc 584 |
1
β’ ((π½ β ran πGen β§
πΉ Fn π) β (π½ qTop πΉ) β ran πGen) |