Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2733 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
3 | 1, 2 | cnf 22613 |
. . . . . 6
β’ (π β (π½ Cn πΎ) β π:βͺ π½βΆβͺ πΎ) |
4 | 3 | adantl 483 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π:βͺ π½βΆβͺ πΎ) |
5 | | cnvimass 6034 |
. . . . . . . . 9
β’ (β‘π β π₯) β dom π |
6 | 4 | fdmd 6680 |
. . . . . . . . . 10
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β dom π = βͺ π½) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β dom π = βͺ π½) |
8 | 5, 7 | sseqtrid 3997 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β βͺ π½) |
9 | | cnvresima 6183 |
. . . . . . . . . . . 12
β’ (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β (π₯ β© (π β π¦))) β© π¦) |
10 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π:βͺ π½βΆβͺ πΎ) |
11 | | ffun 6672 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π½βΆβͺ πΎ
β Fun π) |
12 | | inpreima 7015 |
. . . . . . . . . . . . . . 15
β’ (Fun
π β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
14 | 13 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦)) |
15 | | in32 4182 |
. . . . . . . . . . . . . 14
β’ (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) |
16 | | ssrin 4194 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘π β π₯) β dom π β ((β‘π β π₯) β© π¦) β (dom π β© π¦)) |
17 | 5, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘π β π₯) β© π¦) β (dom π β© π¦) |
18 | | dminss 6106 |
. . . . . . . . . . . . . . . . 17
β’ (dom
π β© π¦) β (β‘π β (π β π¦)) |
19 | 17, 18 | sstri 3954 |
. . . . . . . . . . . . . . . 16
β’ ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦))) |
21 | | df-ss 3928 |
. . . . . . . . . . . . . . 15
β’ (((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
23 | 15, 22 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
24 | 14, 23 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
25 | 9, 24 | eqtrid 2785 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© π¦)) |
26 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn πΎ)) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π
β (π½ Cn πΎ)) |
28 | | elpwi 4568 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π« βͺ π½
β π¦ β βͺ π½) |
29 | 28 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π¦
β βͺ π½) |
30 | 1 | cnrest 22652 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ π¦ β βͺ π½) β (π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
31 | 27, 29, 30 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
32 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β Top) |
33 | 32 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β Top) |
34 | | toptopon2 22283 |
. . . . . . . . . . . . . . 15
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β (TopOnββͺ πΎ)) |
36 | | df-ima 5647 |
. . . . . . . . . . . . . . . 16
β’ (π β π¦) = ran (π βΎ π¦) |
37 | 36 | eqimss2i 4004 |
. . . . . . . . . . . . . . 15
β’ ran
(π βΎ π¦) β (π β π¦) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran (π
βΎ π¦) β (π β π¦)) |
39 | | imassrn 6025 |
. . . . . . . . . . . . . . 15
β’ (π β π¦) β ran π |
40 | 10 | frnd 6677 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran π
β βͺ πΎ) |
41 | 39, 40 | sstrid 3956 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
β π¦) β βͺ πΎ) |
42 | | cnrest2 22653 |
. . . . . . . . . . . . . 14
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran (π βΎ π¦) β (π β π¦) β§ (π β π¦) β βͺ πΎ) β ((π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ) β (π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))))) |
43 | 35, 38, 41, 42 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((π
βΎ π¦) β ((π½ βΎt π¦) Cn πΎ) β (π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))))) |
44 | 31, 43 | mpbid 231 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦)))) |
45 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π₯
β (πGenβπΎ)) |
46 | | simprr 772 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π½
βΎt π¦)
β Comp) |
47 | | imacmp 22764 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ (π½ βΎt π¦) β Comp) β (πΎ βΎt (π β π¦)) β Comp) |
48 | 27, 46, 47 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (πΎ
βΎt (π
β π¦)) β
Comp) |
49 | | kgeni 22904 |
. . . . . . . . . . . . 13
β’ ((π₯ β
(πGenβπΎ)
β§ (πΎ
βΎt (π
β π¦)) β Comp)
β (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
50 | 45, 48, 49 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π₯
β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
51 | | cnima 22632 |
. . . . . . . . . . . 12
β’ (((π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))) β§ (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
52 | 44, 50, 51 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
53 | 25, 52 | eqeltrrd 2835 |
. . . . . . . . . 10
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦)) |
54 | 53 | expr 458 |
. . . . . . . . 9
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ π¦ β π« βͺ π½)
β ((π½
βΎt π¦)
β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
55 | 54 | ralrimiva 3140 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
56 | | kgentop 22909 |
. . . . . . . . . . 11
β’ (π½ β ran πGen β
π½ β
Top) |
57 | 56 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β Top) |
58 | | toptopon2 22283 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
59 | 57, 58 | sylib 217 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β (TopOnββͺ π½)) |
60 | | elkgen 22903 |
. . . . . . . . 9
β’ (π½ β (TopOnββͺ π½)
β ((β‘π β π₯) β (πGenβπ½) β ((β‘π β π₯) β βͺ π½ β§ βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))))) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β ((β‘π β π₯) β (πGenβπ½) β ((β‘π β π₯) β βͺ π½ β§ βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))))) |
62 | 8, 55, 61 | mpbir2and 712 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β (πGenβπ½)) |
63 | | kgenidm 22914 |
. . . . . . . 8
β’ (π½ β ran πGen β
(πGenβπ½) =
π½) |
64 | 63 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (πGenβπ½) = π½) |
65 | 62, 64 | eleqtrd 2836 |
. . . . . 6
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β π½) |
66 | 65 | ralrimiva 3140 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β βπ₯ β (πGenβπΎ)(β‘π β π₯) β π½) |
67 | 56, 58 | sylib 217 |
. . . . . . 7
β’ (π½ β ran πGen β
π½ β (TopOnββͺ π½)) |
68 | | kgentopon 22905 |
. . . . . . . 8
β’ (πΎ β (TopOnββͺ πΎ)
β (πGenβπΎ) β (TopOnββͺ πΎ)) |
69 | 34, 68 | sylbi 216 |
. . . . . . 7
β’ (πΎ β Top β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
70 | | iscn 22602 |
. . . . . . 7
β’ ((π½ β (TopOnββͺ π½)
β§ (πGenβπΎ) β (TopOnββͺ πΎ))
β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
71 | 67, 69, 70 | syl2an 597 |
. . . . . 6
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
72 | 71 | adantr 482 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
73 | 4, 66, 72 | mpbir2and 712 |
. . . 4
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn (πGenβπΎ))) |
74 | 73 | ex 414 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn πΎ) β π β (π½ Cn (πGenβπΎ)))) |
75 | 74 | ssrdv 3951 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) β (π½ Cn (πGenβπΎ))) |
76 | 69 | adantl 483 |
. . . 4
β’ ((π½ β ran πGen β§
πΎ β Top) β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
77 | | toponcom 22293 |
. . . 4
β’ ((πΎ β Top β§
(πGenβπΎ)
β (TopOnββͺ πΎ)) β πΎ β (TopOnββͺ (πGenβπΎ))) |
78 | 32, 76, 77 | syl2anc 585 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β (TopOnββͺ (πGenβπΎ))) |
79 | | kgenss 22910 |
. . . 4
β’ (πΎ β Top β πΎ β
(πGenβπΎ)) |
80 | 79 | adantl 483 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β
(πGenβπΎ)) |
81 | | eqid 2733 |
. . . 4
β’ βͺ (πGenβπΎ) = βͺ
(πGenβπΎ) |
82 | 81 | cnss2 22644 |
. . 3
β’ ((πΎ β (TopOnββͺ (πGenβπΎ)) β§ πΎ β (πGenβπΎ)) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
83 | 78, 80, 82 | syl2anc 585 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
84 | 75, 83 | eqssd 3962 |
1
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) = (π½ Cn (πGenβπΎ))) |