Step | Hyp | Ref
| Expression |
1 | | tgpgrp 23452 |
. . . . 5
β’ (πΊ β TopGrp β πΊ β Grp) |
2 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
3 | | tgphaus.1 |
. . . . . 6
β’ 0 =
(0gβπΊ) |
4 | 2, 3 | grpidcl 18786 |
. . . . 5
β’ (πΊ β Grp β 0 β
(BaseβπΊ)) |
5 | 1, 4 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β 0 β
(BaseβπΊ)) |
6 | | tgphaus.j |
. . . . . 6
β’ π½ = (TopOpenβπΊ) |
7 | 6, 2 | tgptopon 23456 |
. . . . 5
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
8 | | toponuni 22286 |
. . . . 5
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (BaseβπΊ) = βͺ π½) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β
(BaseβπΊ) = βͺ π½) |
10 | 5, 9 | eleqtrd 2836 |
. . 3
β’ (πΊ β TopGrp β 0 β βͺ π½) |
11 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
12 | 11 | sncld 22745 |
. . . 4
β’ ((π½ β Haus β§ 0 β βͺ π½)
β { 0 } β (Clsdβπ½)) |
13 | 12 | expcom 415 |
. . 3
β’ ( 0 β βͺ π½
β (π½ β Haus
β { 0 } β (Clsdβπ½))) |
14 | 10, 13 | syl 17 |
. 2
β’ (πΊ β TopGrp β (π½ β Haus β { 0 } β
(Clsdβπ½))) |
15 | | eqid 2733 |
. . . . . 6
β’
(-gβπΊ) = (-gβπΊ) |
16 | 6, 15 | tgpsubcn 23464 |
. . . . 5
β’ (πΊ β TopGrp β
(-gβπΊ)
β ((π½
Γt π½) Cn
π½)) |
17 | | cnclima 22642 |
. . . . . 6
β’
(((-gβπΊ) β ((π½ Γt π½) Cn π½) β§ { 0 } β (Clsdβπ½)) β (β‘(-gβπΊ) β { 0 }) β
(Clsdβ(π½
Γt π½))) |
18 | 17 | ex 414 |
. . . . 5
β’
((-gβπΊ) β ((π½ Γt π½) Cn π½) β ({ 0 } β (Clsdβπ½) β (β‘(-gβπΊ) β { 0 }) β
(Clsdβ(π½
Γt π½)))) |
19 | 16, 18 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β ({ 0 } β
(Clsdβπ½) β
(β‘(-gβπΊ) β { 0 }) β
(Clsdβ(π½
Γt π½)))) |
20 | | cnvimass 6037 |
. . . . . . . . 9
β’ (β‘(-gβπΊ) β { 0 }) β dom
(-gβπΊ) |
21 | 2, 15 | grpsubf 18834 |
. . . . . . . . . 10
β’ (πΊ β Grp β
(-gβπΊ):((BaseβπΊ) Γ (BaseβπΊ))βΆ(BaseβπΊ)) |
22 | 1, 21 | syl 17 |
. . . . . . . . 9
β’ (πΊ β TopGrp β
(-gβπΊ):((BaseβπΊ) Γ (BaseβπΊ))βΆ(BaseβπΊ)) |
23 | 20, 22 | fssdm 6692 |
. . . . . . . 8
β’ (πΊ β TopGrp β (β‘(-gβπΊ) β { 0 }) β
((BaseβπΊ) Γ
(BaseβπΊ))) |
24 | | relxp 5655 |
. . . . . . . 8
β’ Rel
((BaseβπΊ) Γ
(BaseβπΊ)) |
25 | | relss 5741 |
. . . . . . . 8
β’ ((β‘(-gβπΊ) β { 0 }) β
((BaseβπΊ) Γ
(BaseβπΊ)) β (Rel
((BaseβπΊ) Γ
(BaseβπΊ)) β Rel
(β‘(-gβπΊ) β { 0 }))) |
26 | 23, 24, 25 | mpisyl 21 |
. . . . . . 7
β’ (πΊ β TopGrp β Rel (β‘(-gβπΊ) β { 0 })) |
27 | | dfrel4v 6146 |
. . . . . . 7
β’ (Rel
(β‘(-gβπΊ) β { 0 }) β (β‘(-gβπΊ) β { 0 }) = {β¨π₯, π¦β© β£ π₯(β‘(-gβπΊ) β { 0 })π¦}) |
28 | 26, 27 | sylib 217 |
. . . . . 6
β’ (πΊ β TopGrp β (β‘(-gβπΊ) β { 0 }) = {β¨π₯, π¦β© β£ π₯(β‘(-gβπΊ) β { 0 })π¦}) |
29 | 22 | ffnd 6673 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β
(-gβπΊ) Fn
((BaseβπΊ) Γ
(BaseβπΊ))) |
30 | | elpreima 7012 |
. . . . . . . . . . 11
β’
((-gβπΊ) Fn ((BaseβπΊ) Γ (BaseβπΊ)) β (β¨π₯, π¦β© β (β‘(-gβπΊ) β { 0 }) β (β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ (πΊ β TopGrp β
(β¨π₯, π¦β© β (β‘(-gβπΊ) β { 0 }) β (β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }))) |
32 | | opelxp 5673 |
. . . . . . . . . . . 12
β’
(β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) |
33 | 32 | anbi1i 625 |
. . . . . . . . . . 11
β’
((β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§
((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }) β ((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β { 0 })) |
34 | 2, 3, 15 | grpsubeq0 18841 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β ((π₯(-gβπΊ)π¦) = 0 β π₯ = π¦)) |
35 | 34 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β ((π₯(-gβπΊ)π¦) = 0 β π₯ = π¦)) |
36 | 1, 35 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β ((π₯(-gβπΊ)π¦) = 0 β π₯ = π¦)) |
37 | | df-ov 7364 |
. . . . . . . . . . . . . . 15
β’ (π₯(-gβπΊ)π¦) = ((-gβπΊ)ββ¨π₯, π¦β©) |
38 | 37 | eleq1i 2825 |
. . . . . . . . . . . . . 14
β’ ((π₯(-gβπΊ)π¦) β { 0 } β
((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }) |
39 | | ovex 7394 |
. . . . . . . . . . . . . . 15
β’ (π₯(-gβπΊ)π¦) β V |
40 | 39 | elsn 4605 |
. . . . . . . . . . . . . 14
β’ ((π₯(-gβπΊ)π¦) β { 0 } β (π₯(-gβπΊ)π¦) = 0 ) |
41 | 38, 40 | bitr3i 277 |
. . . . . . . . . . . . 13
β’
(((-gβπΊ)ββ¨π₯, π¦β©) β { 0 } β (π₯(-gβπΊ)π¦) = 0 ) |
42 | | equcom 2022 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β π₯ = π¦) |
43 | 36, 41, 42 | 3bitr4g 314 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β (((-gβπΊ)ββ¨π₯, π¦β©) β { 0 } β π¦ = π₯)) |
44 | 43 | pm5.32da 580 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β (((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }) β ((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ π¦ = π₯))) |
45 | 33, 44 | bitrid 283 |
. . . . . . . . . 10
β’ (πΊ β TopGrp β
((β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§
((-gβπΊ)ββ¨π₯, π¦β©) β { 0 }) β ((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ π¦ = π₯))) |
46 | 31, 45 | bitrd 279 |
. . . . . . . . 9
β’ (πΊ β TopGrp β
(β¨π₯, π¦β© β (β‘(-gβπΊ) β { 0 }) β ((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ π¦ = π₯))) |
47 | | df-br 5110 |
. . . . . . . . 9
β’ (π₯(β‘(-gβπΊ) β { 0 })π¦ β β¨π₯, π¦β© β (β‘(-gβπΊ) β { 0 })) |
48 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (π¦ β (BaseβπΊ) β π₯ β (BaseβπΊ))) |
49 | 48 | biimparc 481 |
. . . . . . . . . . 11
β’ ((π₯ β (BaseβπΊ) β§ π¦ = π₯) β π¦ β (BaseβπΊ)) |
50 | 49 | pm4.71i 561 |
. . . . . . . . . 10
β’ ((π₯ β (BaseβπΊ) β§ π¦ = π₯) β ((π₯ β (BaseβπΊ) β§ π¦ = π₯) β§ π¦ β (BaseβπΊ))) |
51 | | an32 645 |
. . . . . . . . . 10
β’ (((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ π¦ = π₯) β ((π₯ β (BaseβπΊ) β§ π¦ = π₯) β§ π¦ β (BaseβπΊ))) |
52 | 50, 51 | bitr4i 278 |
. . . . . . . . 9
β’ ((π₯ β (BaseβπΊ) β§ π¦ = π₯) β ((π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β§ π¦ = π₯)) |
53 | 46, 47, 52 | 3bitr4g 314 |
. . . . . . . 8
β’ (πΊ β TopGrp β (π₯(β‘(-gβπΊ) β { 0 })π¦ β (π₯ β (BaseβπΊ) β§ π¦ = π₯))) |
54 | 53 | opabbidv 5175 |
. . . . . . 7
β’ (πΊ β TopGrp β
{β¨π₯, π¦β© β£ π₯(β‘(-gβπΊ) β { 0 })π¦} = {β¨π₯, π¦β© β£ (π₯ β (BaseβπΊ) β§ π¦ = π₯)}) |
55 | | opabresid 6007 |
. . . . . . 7
β’ ( I
βΎ (BaseβπΊ)) =
{β¨π₯, π¦β© β£ (π₯ β (BaseβπΊ) β§ π¦ = π₯)} |
56 | 54, 55 | eqtr4di 2791 |
. . . . . 6
β’ (πΊ β TopGrp β
{β¨π₯, π¦β© β£ π₯(β‘(-gβπΊ) β { 0 })π¦} = ( I βΎ (BaseβπΊ))) |
57 | 9 | reseq2d 5941 |
. . . . . 6
β’ (πΊ β TopGrp β ( I
βΎ (BaseβπΊ)) = (
I βΎ βͺ π½)) |
58 | 28, 56, 57 | 3eqtrd 2777 |
. . . . 5
β’ (πΊ β TopGrp β (β‘(-gβπΊ) β { 0 }) = ( I βΎ βͺ π½)) |
59 | 58 | eleq1d 2819 |
. . . 4
β’ (πΊ β TopGrp β ((β‘(-gβπΊ) β { 0 }) β
(Clsdβ(π½
Γt π½))
β ( I βΎ βͺ π½) β (Clsdβ(π½ Γt π½)))) |
60 | 19, 59 | sylibd 238 |
. . 3
β’ (πΊ β TopGrp β ({ 0 } β
(Clsdβπ½) β ( I
βΎ βͺ π½) β (Clsdβ(π½ Γt π½)))) |
61 | | topontop 22285 |
. . . . 5
β’ (π½ β
(TopOnβ(BaseβπΊ)) β π½ β Top) |
62 | 7, 61 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β π½ β Top) |
63 | 11 | hausdiag 23019 |
. . . . 5
β’ (π½ β Haus β (π½ β Top β§ ( I βΎ
βͺ π½) β (Clsdβ(π½ Γt π½)))) |
64 | 63 | baib 537 |
. . . 4
β’ (π½ β Top β (π½ β Haus β ( I βΎ
βͺ π½) β (Clsdβ(π½ Γt π½)))) |
65 | 62, 64 | syl 17 |
. . 3
β’ (πΊ β TopGrp β (π½ β Haus β ( I βΎ
βͺ π½) β (Clsdβ(π½ Γt π½)))) |
66 | 60, 65 | sylibrd 259 |
. 2
β’ (πΊ β TopGrp β ({ 0 } β
(Clsdβπ½) β π½ β Haus)) |
67 | 14, 66 | impbid 211 |
1
β’ (πΊ β TopGrp β (π½ β Haus β { 0 } β
(Clsdβπ½))) |