Step | Hyp | Ref
| Expression |
1 | | kgenf 22915 |
. . . 4
β’
πGen:TopβΆTop |
2 | | ffn 6672 |
. . . 4
β’
(πGen:TopβΆTop β πGen Fn
Top) |
3 | | fvelrnb 6907 |
. . . 4
β’
(πGen Fn Top β (π½ β ran πGen β βπ β Top
(πGenβπ) =
π½)) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
β’ (π½ β ran πGen β
βπ β Top
(πGenβπ) =
π½) |
5 | | toptopon2 22290 |
. . . . . . . . . . 11
β’ (π β Top β π β (TopOnββͺ π)) |
6 | | kgentopon 22912 |
. . . . . . . . . . 11
β’ (π β (TopOnββͺ π)
β (πGenβπ) β (TopOnββͺ π)) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . . 10
β’ (π β Top β
(πGenβπ)
β (TopOnββͺ π)) |
8 | | kgentopon 22912 |
. . . . . . . . . 10
β’
((πGenβπ) β (TopOnββͺ π)
β (πGenβ(πGenβπ)) β (TopOnββͺ π)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ (π β Top β
(πGenβ(πGenβπ)) β (TopOnββͺ π)) |
10 | | toponss 22299 |
. . . . . . . . 9
β’
(((πGenβ(πGenβπ)) β (TopOnββͺ π)
β§ π₯ β
(πGenβ(πGenβπ))) β π₯ β βͺ π) |
11 | 9, 10 | sylan 581 |
. . . . . . . 8
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β π₯ β βͺ π) |
12 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π₯
β (πGenβ(πGenβπ))) |
13 | | kgencmp2 22920 |
. . . . . . . . . . . . . 14
β’ (π β Top β ((π βΎt π) β Comp β
((πGenβπ)
βΎt π)
β Comp)) |
14 | 13 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((π β Top β§ (π βΎt π) β Comp) β
((πGenβπ)
βΎt π)
β Comp) |
15 | 14 | ad2ant2rl 748 |
. . . . . . . . . . . 12
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((πGenβπ) βΎt π) β Comp) |
16 | | kgeni 22911 |
. . . . . . . . . . . 12
β’ ((π₯ β
(πGenβ(πGenβπ)) β§ ((πGenβπ) βΎt π) β Comp) β (π₯ β© π) β ((πGenβπ) βΎt π)) |
17 | 12, 15, 16 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π₯
β© π) β
((πGenβπ)
βΎt π)) |
18 | | kgencmp 22919 |
. . . . . . . . . . . 12
β’ ((π β Top β§ (π βΎt π) β Comp) β (π βΎt π) = ((πGenβπ) βΎt π)) |
19 | 18 | ad2ant2rl 748 |
. . . . . . . . . . 11
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
βΎt π) =
((πGenβπ)
βΎt π)) |
20 | 17, 19 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π₯
β© π) β (π βΎt π)) |
21 | 20 | expr 458 |
. . . . . . . . 9
β’ (((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β§ π β π« βͺ π)
β ((π
βΎt π)
β Comp β (π₯ β©
π) β (π βΎt π))) |
22 | 21 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β βπ β π« βͺ π((π βΎt π) β Comp β (π₯ β© π) β (π βΎt π))) |
23 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β π β Top) |
24 | 23, 5 | sylib 217 |
. . . . . . . . 9
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β π β (TopOnββͺ π)) |
25 | | elkgen 22910 |
. . . . . . . . 9
β’ (π β (TopOnββͺ π)
β (π₯ β
(πGenβπ)
β (π₯ β βͺ π
β§ βπ β
π« βͺ π((π βΎt π) β Comp β (π₯ β© π) β (π βΎt π))))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β (π₯ β (πGenβπ) β (π₯ β βͺ π β§ βπ β π« βͺ π((π βΎt π) β Comp β (π₯ β© π) β (π βΎt π))))) |
27 | 11, 22, 26 | mpbir2and 712 |
. . . . . . 7
β’ ((π β Top β§ π₯ β
(πGenβ(πGenβπ))) β π₯ β (πGenβπ)) |
28 | 27 | ex 414 |
. . . . . 6
β’ (π β Top β (π₯ β
(πGenβ(πGenβπ)) β π₯ β (πGenβπ))) |
29 | 28 | ssrdv 3954 |
. . . . 5
β’ (π β Top β
(πGenβ(πGenβπ)) β (πGenβπ)) |
30 | | fveq2 6846 |
. . . . . 6
β’
((πGenβπ) = π½ β
(πGenβ(πGenβπ)) = (πGenβπ½)) |
31 | | id 22 |
. . . . . 6
β’
((πGenβπ) = π½ β (πGenβπ) = π½) |
32 | 30, 31 | sseq12d 3981 |
. . . . 5
β’
((πGenβπ) = π½ β
((πGenβ(πGenβπ)) β (πGenβπ) β
(πGenβπ½)
β π½)) |
33 | 29, 32 | syl5ibcom 244 |
. . . 4
β’ (π β Top β
((πGenβπ) =
π½ β
(πGenβπ½)
β π½)) |
34 | 33 | rexlimiv 3142 |
. . 3
β’
(βπ β Top
(πGenβπ) =
π½ β
(πGenβπ½)
β π½) |
35 | 4, 34 | sylbi 216 |
. 2
β’ (π½ β ran πGen β
(πGenβπ½)
β π½) |
36 | | kgentop 22916 |
. . 3
β’ (π½ β ran πGen β
π½ β
Top) |
37 | | kgenss 22917 |
. . 3
β’ (π½ β Top β π½ β
(πGenβπ½)) |
38 | 36, 37 | syl 17 |
. 2
β’ (π½ β ran πGen β
π½ β
(πGenβπ½)) |
39 | 35, 38 | eqssd 3965 |
1
β’ (π½ β ran πGen β
(πGenβπ½) =
π½) |