Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2731 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
3 | 1, 2 | cnf 22971 |
. . . . . 6
β’ (π β (π½ Cn πΎ) β π:βͺ π½βΆβͺ πΎ) |
4 | 3 | adantl 481 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π:βͺ π½βΆβͺ πΎ) |
5 | | cnvimass 6080 |
. . . . . . . . 9
β’ (β‘π β π₯) β dom π |
6 | 4 | fdmd 6728 |
. . . . . . . . . 10
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β dom π = βͺ π½) |
7 | 6 | adantr 480 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β dom π = βͺ π½) |
8 | 5, 7 | sseqtrid 4034 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β βͺ π½) |
9 | | cnvresima 6229 |
. . . . . . . . . . . 12
β’ (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β (π₯ β© (π β π¦))) β© π¦) |
10 | 4 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π:βͺ π½βΆβͺ πΎ) |
11 | | ffun 6720 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π½βΆβͺ πΎ
β Fun π) |
12 | | inpreima 7065 |
. . . . . . . . . . . . . . 15
β’ (Fun
π β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
14 | 13 | ineq1d 4211 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦)) |
15 | | in32 4221 |
. . . . . . . . . . . . . 14
β’ (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) |
16 | | ssrin 4233 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘π β π₯) β dom π β ((β‘π β π₯) β© π¦) β (dom π β© π¦)) |
17 | 5, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘π β π₯) β© π¦) β (dom π β© π¦) |
18 | | dminss 6152 |
. . . . . . . . . . . . . . . . 17
β’ (dom
π β© π¦) β (β‘π β (π β π¦)) |
19 | 17, 18 | sstri 3991 |
. . . . . . . . . . . . . . . 16
β’ ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦))) |
21 | | df-ss 3965 |
. . . . . . . . . . . . . . 15
β’ (((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
23 | 15, 22 | eqtrid 2783 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
24 | 14, 23 | eqtrd 2771 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
25 | 9, 24 | eqtrid 2783 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© π¦)) |
26 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn πΎ)) |
27 | 26 | ad2antrr 723 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π
β (π½ Cn πΎ)) |
28 | | elpwi 4609 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π« βͺ π½
β π¦ β βͺ π½) |
29 | 28 | ad2antrl 725 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π¦
β βͺ π½) |
30 | 1 | cnrest 23010 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ π¦ β βͺ π½) β (π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
31 | 27, 29, 30 | syl2anc 583 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
32 | | simpr 484 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β Top) |
33 | 32 | ad3antrrr 727 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β Top) |
34 | | toptopon2 22641 |
. . . . . . . . . . . . . . 15
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β (TopOnββͺ πΎ)) |
36 | | df-ima 5689 |
. . . . . . . . . . . . . . . 16
β’ (π β π¦) = ran (π βΎ π¦) |
37 | 36 | eqimss2i 4043 |
. . . . . . . . . . . . . . 15
β’ ran
(π βΎ π¦) β (π β π¦) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran (π
βΎ π¦) β (π β π¦)) |
39 | | imassrn 6070 |
. . . . . . . . . . . . . . 15
β’ (π β π¦) β ran π |
40 | 10 | frnd 6725 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran π
β βͺ πΎ) |
41 | 39, 40 | sstrid 3993 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
β π¦) β βͺ πΎ) |
42 | | cnrest2 23011 |
. . . . . . . . . . . . . 14
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran (π βΎ π¦) β (π β π¦) β§ (π β π¦) β βͺ πΎ) β ((π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ) β (π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))))) |
43 | 35, 38, 41, 42 | syl3anc 1370 |
. . . . . . . . . . . . 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 766 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π₯
β (πGenβπΎ)) |
46 | | simprr 770 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π½
βΎt π¦)
β Comp) |
47 | | imacmp 23122 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ (π½ βΎt π¦) β Comp) β (πΎ βΎt (π β π¦)) β Comp) |
48 | 27, 46, 47 | syl2anc 583 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (πΎ
βΎt (π
β π¦)) β
Comp) |
49 | | kgeni 23262 |
. . . . . . . . . . . . 13
β’ ((π₯ β
(πGenβπΎ)
β§ (πΎ
βΎt (π
β π¦)) β Comp)
β (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
50 | 45, 48, 49 | syl2anc 583 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π₯
β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
51 | | cnima 22990 |
. . . . . . . . . . . 12
β’ (((π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))) β§ (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
52 | 44, 50, 51 | syl2anc 583 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
53 | 25, 52 | eqeltrrd 2833 |
. . . . . . . . . 10
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦)) |
54 | 53 | expr 456 |
. . . . . . . . 9
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ π¦ β π« βͺ π½)
β ((π½
βΎt π¦)
β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
55 | 54 | ralrimiva 3145 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
56 | | kgentop 23267 |
. . . . . . . . . . 11
β’ (π½ β ran πGen β
π½ β
Top) |
57 | 56 | ad3antrrr 727 |
. . . . . . . . . 10
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β Top) |
58 | | toptopon2 22641 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
59 | 57, 58 | sylib 217 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β (TopOnββͺ π½)) |
60 | | elkgen 23261 |
. . . . . . . . 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 710 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β (πGenβπ½)) |
63 | | kgenidm 23272 |
. . . . . . . 8
β’ (π½ β ran πGen β
(πGenβπ½) =
π½) |
64 | 63 | ad3antrrr 727 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (πGenβπ½) = π½) |
65 | 62, 64 | eleqtrd 2834 |
. . . . . 6
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β π½) |
66 | 65 | ralrimiva 3145 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β βπ₯ β (πGenβπΎ)(β‘π β π₯) β π½) |
67 | 56, 58 | sylib 217 |
. . . . . . 7
β’ (π½ β ran πGen β
π½ β (TopOnββͺ π½)) |
68 | | kgentopon 23263 |
. . . . . . . 8
β’ (πΎ β (TopOnββͺ πΎ)
β (πGenβπΎ) β (TopOnββͺ πΎ)) |
69 | 34, 68 | sylbi 216 |
. . . . . . 7
β’ (πΎ β Top β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
70 | | iscn 22960 |
. . . . . . 7
β’ ((π½ β (TopOnββͺ π½)
β§ (πGenβπΎ) β (TopOnββͺ πΎ))
β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
71 | 67, 69, 70 | syl2an 595 |
. . . . . 6
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
72 | 71 | adantr 480 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
73 | 4, 66, 72 | mpbir2and 710 |
. . . 4
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn (πGenβπΎ))) |
74 | 73 | ex 412 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn πΎ) β π β (π½ Cn (πGenβπΎ)))) |
75 | 74 | ssrdv 3988 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) β (π½ Cn (πGenβπΎ))) |
76 | 69 | adantl 481 |
. . . 4
β’ ((π½ β ran πGen β§
πΎ β Top) β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
77 | | toponcom 22651 |
. . . 4
β’ ((πΎ β Top β§
(πGenβπΎ)
β (TopOnββͺ πΎ)) β πΎ β (TopOnββͺ (πGenβπΎ))) |
78 | 32, 76, 77 | syl2anc 583 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β (TopOnββͺ (πGenβπΎ))) |
79 | | kgenss 23268 |
. . . 4
β’ (πΎ β Top β πΎ β
(πGenβπΎ)) |
80 | 79 | adantl 481 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β
(πGenβπΎ)) |
81 | | eqid 2731 |
. . . 4
β’ βͺ (πGenβπΎ) = βͺ
(πGenβπΎ) |
82 | 81 | cnss2 23002 |
. . 3
β’ ((πΎ β (TopOnββͺ (πGenβπΎ)) β§ πΎ β (πGenβπΎ)) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
83 | 78, 80, 82 | syl2anc 583 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
84 | 75, 83 | eqssd 3999 |
1
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) = (π½ Cn (πGenβπΎ))) |