Step | Hyp | Ref
| Expression |
1 | | eqid 2730 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2730 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
3 | 1, 2 | cnf 22970 |
. . . . . 6
β’ (π β (π½ Cn πΎ) β π:βͺ π½βΆβͺ πΎ) |
4 | 3 | adantl 480 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π:βͺ π½βΆβͺ πΎ) |
5 | | cnvimass 6079 |
. . . . . . . . 9
β’ (β‘π β π₯) β dom π |
6 | 4 | fdmd 6727 |
. . . . . . . . . 10
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β dom π = βͺ π½) |
7 | 6 | adantr 479 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β dom π = βͺ π½) |
8 | 5, 7 | sseqtrid 4033 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β βͺ π½) |
9 | | cnvresima 6228 |
. . . . . . . . . . . 12
β’ (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β (π₯ β© (π β π¦))) β© π¦) |
10 | 4 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π:βͺ π½βΆβͺ πΎ) |
11 | | ffun 6719 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π½βΆβͺ πΎ
β Fun π) |
12 | | inpreima 7064 |
. . . . . . . . . . . . . . 15
β’ (Fun
π β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘π β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© (β‘π β (π β π¦)))) |
14 | 13 | ineq1d 4210 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦)) |
15 | | in32 4220 |
. . . . . . . . . . . . . 14
β’ (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) |
16 | | ssrin 4232 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘π β π₯) β dom π β ((β‘π β π₯) β© π¦) β (dom π β© π¦)) |
17 | 5, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘π β π₯) β© π¦) β (dom π β© π¦) |
18 | | dminss 6151 |
. . . . . . . . . . . . . . . . 17
β’ (dom
π β© π¦) β (β‘π β (π β π¦)) |
19 | 17, 18 | sstri 3990 |
. . . . . . . . . . . . . . . 16
β’ ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (β‘π β (π β π¦))) |
21 | | df-ss 3964 |
. . . . . . . . . . . . . . 15
β’ (((β‘π β π₯) β© π¦) β (β‘π β (π β π¦)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© π¦) β© (β‘π β (π β π¦))) = ((β‘π β π₯) β© π¦)) |
23 | 15, 22 | eqtrid 2782 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (((β‘π β π₯) β© (β‘π β (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
24 | 14, 23 | eqtrd 2770 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β (π₯ β© (π β π¦))) β© π¦) = ((β‘π β π₯) β© π¦)) |
25 | 9, 24 | eqtrid 2782 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) = ((β‘π β π₯) β© π¦)) |
26 | | simpr 483 |
. . . . . . . . . . . . . . 15
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn πΎ)) |
27 | 26 | ad2antrr 722 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π
β (π½ Cn πΎ)) |
28 | | elpwi 4608 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π« βͺ π½
β π¦ β βͺ π½) |
29 | 28 | ad2antrl 724 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π¦
β βͺ π½) |
30 | 1 | cnrest 23009 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ π¦ β βͺ π½) β (π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
31 | 27, 29, 30 | syl2anc 582 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
βΎ π¦) β ((π½ βΎt π¦) Cn πΎ)) |
32 | | simpr 483 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β Top) |
33 | 32 | ad3antrrr 726 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β Top) |
34 | | toptopon2 22640 |
. . . . . . . . . . . . . . 15
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β πΎ
β (TopOnββͺ πΎ)) |
36 | | df-ima 5688 |
. . . . . . . . . . . . . . . 16
β’ (π β π¦) = ran (π βΎ π¦) |
37 | 36 | eqimss2i 4042 |
. . . . . . . . . . . . . . 15
β’ ran
(π βΎ π¦) β (π β π¦) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran (π
βΎ π¦) β (π β π¦)) |
39 | | imassrn 6069 |
. . . . . . . . . . . . . . 15
β’ (π β π¦) β ran π |
40 | 10 | frnd 6724 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ran π
β βͺ πΎ) |
41 | 39, 40 | sstrid 3992 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π
β π¦) β βͺ πΎ) |
42 | | cnrest2 23010 |
. . . . . . . . . . . . . 14
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran (π βΎ π¦) β (π β π¦) β§ (π β π¦) β βͺ πΎ) β ((π βΎ π¦) β ((π½ βΎt π¦) Cn πΎ) β (π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))))) |
43 | 35, 38, 41, 42 | syl3anc 1369 |
. . . . . . . . . . . . 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 765 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β π₯
β (πGenβπΎ)) |
46 | | simprr 769 |
. . . . . . . . . . . . . 14
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π½
βΎt π¦)
β Comp) |
47 | | imacmp 23121 |
. . . . . . . . . . . . . 14
β’ ((π β (π½ Cn πΎ) β§ (π½ βΎt π¦) β Comp) β (πΎ βΎt (π β π¦)) β Comp) |
48 | 27, 46, 47 | syl2anc 582 |
. . . . . . . . . . . . 13
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (πΎ
βΎt (π
β π¦)) β
Comp) |
49 | | kgeni 23261 |
. . . . . . . . . . . . 13
β’ ((π₯ β
(πGenβπΎ)
β§ (πΎ
βΎt (π
β π¦)) β Comp)
β (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
50 | 45, 48, 49 | syl2anc 582 |
. . . . . . . . . . . 12
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (π₯
β© (π β π¦)) β (πΎ βΎt (π β π¦))) |
51 | | cnima 22989 |
. . . . . . . . . . . 12
β’ (((π βΎ π¦) β ((π½ βΎt π¦) Cn (πΎ βΎt (π β π¦))) β§ (π₯ β© (π β π¦)) β (πΎ βΎt (π β π¦))) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
52 | 44, 50, 51 | syl2anc 582 |
. . . . . . . . . . 11
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β (β‘(π βΎ π¦) β (π₯ β© (π β π¦))) β (π½ βΎt π¦)) |
53 | 25, 52 | eqeltrrd 2832 |
. . . . . . . . . 10
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ (π¦ β π« βͺ π½
β§ (π½
βΎt π¦)
β Comp)) β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦)) |
54 | 53 | expr 455 |
. . . . . . . . 9
β’
(((((π½ β ran
πGen β§ πΎ β
Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β§ π¦ β π« βͺ π½)
β ((π½
βΎt π¦)
β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
55 | 54 | ralrimiva 3144 |
. . . . . . . 8
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β ((β‘π β π₯) β© π¦) β (π½ βΎt π¦))) |
56 | | kgentop 23266 |
. . . . . . . . . . 11
β’ (π½ β ran πGen β
π½ β
Top) |
57 | 56 | ad3antrrr 726 |
. . . . . . . . . 10
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β Top) |
58 | | toptopon2 22640 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
59 | 57, 58 | sylib 217 |
. . . . . . . . 9
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β π½ β (TopOnββͺ π½)) |
60 | | elkgen 23260 |
. . . . . . . . 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 709 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β (πGenβπ½)) |
63 | | kgenidm 23271 |
. . . . . . . 8
β’ (π½ β ran πGen β
(πGenβπ½) =
π½) |
64 | 63 | ad3antrrr 726 |
. . . . . . 7
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (πGenβπ½) = π½) |
65 | 62, 64 | eleqtrd 2833 |
. . . . . 6
β’ ((((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β§ π₯ β (πGenβπΎ)) β (β‘π β π₯) β π½) |
66 | 65 | ralrimiva 3144 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β βπ₯ β (πGenβπΎ)(β‘π β π₯) β π½) |
67 | 56, 58 | sylib 217 |
. . . . . . 7
β’ (π½ β ran πGen β
π½ β (TopOnββͺ π½)) |
68 | | kgentopon 23262 |
. . . . . . . 8
β’ (πΎ β (TopOnββͺ πΎ)
β (πGenβπΎ) β (TopOnββͺ πΎ)) |
69 | 34, 68 | sylbi 216 |
. . . . . . 7
β’ (πΎ β Top β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
70 | | iscn 22959 |
. . . . . . 7
β’ ((π½ β (TopOnββͺ π½)
β§ (πGenβπΎ) β (TopOnββͺ πΎ))
β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
71 | 67, 69, 70 | syl2an 594 |
. . . . . 6
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
72 | 71 | adantr 479 |
. . . . 5
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β (π β (π½ Cn (πGenβπΎ)) β (π:βͺ π½βΆβͺ πΎ
β§ βπ₯ β
(πGenβπΎ)(β‘π β π₯) β π½))) |
73 | 4, 66, 72 | mpbir2and 709 |
. . . 4
β’ (((π½ β ran πGen β§
πΎ β Top) β§ π β (π½ Cn πΎ)) β π β (π½ Cn (πGenβπΎ))) |
74 | 73 | ex 411 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β (π β (π½ Cn πΎ) β π β (π½ Cn (πGenβπΎ)))) |
75 | 74 | ssrdv 3987 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) β (π½ Cn (πGenβπΎ))) |
76 | 69 | adantl 480 |
. . . 4
β’ ((π½ β ran πGen β§
πΎ β Top) β
(πGenβπΎ)
β (TopOnββͺ πΎ)) |
77 | | toponcom 22650 |
. . . 4
β’ ((πΎ β Top β§
(πGenβπΎ)
β (TopOnββͺ πΎ)) β πΎ β (TopOnββͺ (πGenβπΎ))) |
78 | 32, 76, 77 | syl2anc 582 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β (TopOnββͺ (πGenβπΎ))) |
79 | | kgenss 23267 |
. . . 4
β’ (πΎ β Top β πΎ β
(πGenβπΎ)) |
80 | 79 | adantl 480 |
. . 3
β’ ((π½ β ran πGen β§
πΎ β Top) β πΎ β
(πGenβπΎ)) |
81 | | eqid 2730 |
. . . 4
β’ βͺ (πGenβπΎ) = βͺ
(πGenβπΎ) |
82 | 81 | cnss2 23001 |
. . 3
β’ ((πΎ β (TopOnββͺ (πGenβπΎ)) β§ πΎ β (πGenβπΎ)) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
83 | 78, 80, 82 | syl2anc 582 |
. 2
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn (πGenβπΎ)) β (π½ Cn πΎ)) |
84 | 75, 83 | eqssd 3998 |
1
β’ ((π½ β ran πGen β§
πΎ β Top) β (π½ Cn πΎ) = (π½ Cn (πGenβπΎ))) |