Step | Hyp | Ref
| Expression |
1 | | dfec2 8654 |
. . . . 5
β’ (π΄ β π β [π΄] βΌ = {π§ β£ π΄ βΌ π§}) |
2 | 1 | adantl 483 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = {π§ β£ π΄ βΌ π§}) |
3 | | tgpconncomp.s |
. . . . . . . . 9
β’ π = βͺ
{π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} |
4 | | ssrab2 4038 |
. . . . . . . . . 10
β’ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π |
5 | | sspwuni 5061 |
. . . . . . . . . 10
β’ ({π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π β βͺ {π₯
β π« π β£
( 0
β π₯ β§ (π½ βΎt π₯) β Conn)} β π) |
6 | 4, 5 | mpbi 229 |
. . . . . . . . 9
β’ βͺ {π₯
β π« π β£
( 0
β π₯ β§ (π½ βΎt π₯) β Conn)} β π |
7 | 3, 6 | eqsstri 3979 |
. . . . . . . 8
β’ π β π |
8 | 7 | a1i 11 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π΄ β π) β π β π) |
9 | | tgpconncomp.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπΊ) = (invgβπΊ) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
12 | | tgpconncompeqg.r |
. . . . . . . 8
β’ βΌ =
(πΊ ~QG
π) |
13 | 9, 10, 11, 12 | eqgval 18984 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π β π) β (π΄ βΌ π§ β (π΄ β π β§ π§ β π β§ (((invgβπΊ)βπ΄)(+gβπΊ)π§) β π))) |
14 | 8, 13 | syldan 592 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β (π΄ βΌ π§ β (π΄ β π β§ π§ β π β§ (((invgβπΊ)βπ΄)(+gβπΊ)π§) β π))) |
15 | | simp2 1138 |
. . . . . 6
β’ ((π΄ β π β§ π§ β π β§ (((invgβπΊ)βπ΄)(+gβπΊ)π§) β π) β π§ β π) |
16 | 14, 15 | syl6bi 253 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (π΄ βΌ π§ β π§ β π)) |
17 | 16 | abssdv 4026 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β {π§ β£ π΄ βΌ π§} β π) |
18 | 2, 17 | eqsstrd 3983 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ β π) |
19 | | simpr 486 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β π΄ β π) |
20 | | tgpgrp 23445 |
. . . . . . 7
β’ (πΊ β TopGrp β πΊ β Grp) |
21 | | tgpconncomp.z |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
22 | 9, 11, 21, 10 | grplinv 18805 |
. . . . . . 7
β’ ((πΊ β Grp β§ π΄ β π) β (((invgβπΊ)βπ΄)(+gβπΊ)π΄) = 0 ) |
23 | 20, 22 | sylan 581 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β (((invgβπΊ)βπ΄)(+gβπΊ)π΄) = 0 ) |
24 | | tgpconncomp.j |
. . . . . . . . 9
β’ π½ = (TopOpenβπΊ) |
25 | 24, 9 | tgptopon 23449 |
. . . . . . . 8
β’ (πΊ β TopGrp β π½ β (TopOnβπ)) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π΄ β π) β π½ β (TopOnβπ)) |
27 | 20 | adantr 482 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π΄ β π) β πΊ β Grp) |
28 | 9, 21 | grpidcl 18783 |
. . . . . . . 8
β’ (πΊ β Grp β 0 β π) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π΄ β π) β 0 β π) |
30 | 3 | conncompid 22798 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ 0 β π) β 0 β π) |
31 | 26, 29, 30 | syl2anc 585 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β 0 β π) |
32 | 23, 31 | eqeltrd 2834 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (((invgβπΊ)βπ΄)(+gβπΊ)π΄) β π) |
33 | 9, 10, 11, 12 | eqgval 18984 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β π) β (π΄ βΌ π΄ β (π΄ β π β§ π΄ β π β§ (((invgβπΊ)βπ΄)(+gβπΊ)π΄) β π))) |
34 | 8, 33 | syldan 592 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (π΄ βΌ π΄ β (π΄ β π β§ π΄ β π β§ (((invgβπΊ)βπ΄)(+gβπΊ)π΄) β π))) |
35 | 19, 19, 32, 34 | mpbir3and 1343 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β π΄ βΌ π΄) |
36 | | elecg 8694 |
. . . . 5
β’ ((π΄ β π β§ π΄ β π) β (π΄ β [π΄] βΌ β π΄ βΌ π΄)) |
37 | 19, 19, 36 | syl2anc 585 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β (π΄ β [π΄] βΌ β π΄ βΌ π΄)) |
38 | 35, 37 | mpbird 257 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β π΄ β [π΄] βΌ ) |
39 | 9, 12, 11 | eqglact 18986 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β π β§ π΄ β π) β [π΄] βΌ = ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
40 | 7, 39 | mp3an2 1450 |
. . . . . 6
β’ ((πΊ β Grp β§ π΄ β π) β [π΄] βΌ = ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
41 | 20, 40 | sylan 581 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
42 | 41 | oveq2d 7374 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β (π½ βΎt [π΄] βΌ ) = (π½ βΎt ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π))) |
43 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
44 | | eqid 2733 |
. . . . . . 7
β’ (π§ β π β¦ (π΄(+gβπΊ)π§)) = (π§ β π β¦ (π΄(+gβπΊ)π§)) |
45 | 44, 9, 11, 24 | tgplacthmeo 23470 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β (π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½Homeoπ½)) |
46 | | hmeocn 23127 |
. . . . . 6
β’ ((π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½Homeoπ½) β (π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½ Cn π½)) |
47 | 45, 46 | syl 17 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½ Cn π½)) |
48 | | toponuni 22279 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
49 | 26, 48 | syl 17 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β π = βͺ π½) |
50 | 7, 49 | sseqtrid 3997 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β π β βͺ π½) |
51 | 3 | conncompconn 22799 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ 0 β π) β (π½ βΎt π) β Conn) |
52 | 26, 29, 51 | syl2anc 585 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (π½ βΎt π) β Conn) |
53 | 43, 47, 50, 52 | connima 22792 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β (π½ βΎt ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) β Conn) |
54 | 42, 53 | eqeltrd 2834 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β (π½ βΎt [π΄] βΌ ) β
Conn) |
55 | | eqid 2733 |
. . . 4
β’ βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} = βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} |
56 | 55 | conncompss 22800 |
. . 3
β’ (([π΄] βΌ β π β§ π΄ β [π΄] βΌ β§ (π½ βΎt [π΄] βΌ ) β Conn)
β [π΄] βΌ
β βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) |
57 | 18, 38, 54, 56 | syl3anc 1372 |
. 2
β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ β βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) |
58 | | elpwi 4568 |
. . . . . 6
β’ (π¦ β π« π β π¦ β π) |
59 | 44 | mptpreima 6191 |
. . . . . . . . . . 11
β’ (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) = {π§ β π β£ (π΄(+gβπΊ)π§) β π¦} |
60 | 59 | ssrab3 4041 |
. . . . . . . . . 10
β’ (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π |
61 | 29 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β 0 β π) |
62 | 9, 11, 21 | grprid 18786 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π΄ β π) β (π΄(+gβπΊ) 0 ) = π΄) |
63 | 20, 62 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π΄ β π) β (π΄(+gβπΊ) 0 ) = π΄) |
64 | 63 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (π΄(+gβπΊ) 0 ) = π΄) |
65 | | simprrl 780 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π΄ β π¦) |
66 | 64, 65 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (π΄(+gβπΊ) 0 ) β π¦) |
67 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π§ = 0 β (π΄(+gβπΊ)π§) = (π΄(+gβπΊ) 0 )) |
68 | 67 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π§ = 0 β ((π΄(+gβπΊ)π§) β π¦ β (π΄(+gβπΊ) 0 ) β π¦)) |
69 | 68, 59 | elrab2 3649 |
. . . . . . . . . . 11
β’ ( 0 β (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β ( 0 β π β§ (π΄(+gβπΊ) 0 ) β π¦)) |
70 | 61, 66, 69 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β 0 β (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦)) |
71 | | hmeocnvcn 23128 |
. . . . . . . . . . . . 13
β’ ((π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½Homeoπ½) β β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½ Cn π½)) |
72 | 45, 71 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π΄ β π) β β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½ Cn π½)) |
73 | 72 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β (π½ Cn π½)) |
74 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π¦ β π) |
75 | 49 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π = βͺ π½) |
76 | 74, 75 | sseqtrd 3985 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π¦ β βͺ π½) |
77 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (π½ βΎt π¦) β Conn) |
78 | 43, 73, 76, 77 | connima 22792 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (π½ βΎt (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦)) β Conn) |
79 | 3 | conncompss 22800 |
. . . . . . . . . 10
β’ (((β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π β§ 0 β (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β§ (π½ βΎt (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦)) β Conn) β (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π) |
80 | 60, 70, 78, 79 | mp3an2i 1467 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π) |
81 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§))) = (π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§))) |
82 | 81, 9, 11, 10 | grplactcnv 18855 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ π΄ β π) β (((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄):πβ1-1-ontoβπ β§ β‘((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄) = ((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))β((invgβπΊ)βπ΄)))) |
83 | 20, 82 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π΄ β π) β (((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄):πβ1-1-ontoβπ β§ β‘((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄) = ((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))β((invgβπΊ)βπ΄)))) |
84 | 83 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π΄ β π) β ((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄):πβ1-1-ontoβπ) |
85 | 81, 9 | grplactfval 18853 |
. . . . . . . . . . . . . . 15
β’ (π΄ β π β ((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄) = (π§ β π β¦ (π΄(+gβπΊ)π§))) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π΄ β π) β ((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄) = (π§ β π β¦ (π΄(+gβπΊ)π§))) |
87 | 86 | f1oeq1d 6780 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π΄ β π) β (((π β π β¦ (π§ β π β¦ (π(+gβπΊ)π§)))βπ΄):πβ1-1-ontoβπ β (π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ)) |
88 | 84, 87 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π΄ β π) β (π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β (π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ) |
90 | | f1ocnv 6797 |
. . . . . . . . . . 11
β’ ((π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ β β‘(π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ) |
91 | | f1ofun 6787 |
. . . . . . . . . . 11
β’ (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ β Fun β‘(π§ β π β¦ (π΄(+gβπΊ)π§))) |
92 | 89, 90, 91 | 3syl 18 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β Fun β‘(π§ β π β¦ (π΄(+gβπΊ)π§))) |
93 | | f1odm 6789 |
. . . . . . . . . . . 12
β’ (β‘(π§ β π β¦ (π΄(+gβπΊ)π§)):πβ1-1-ontoβπ β dom β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) = π) |
94 | 89, 90, 93 | 3syl 18 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β dom β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) = π) |
95 | 74, 94 | sseqtrrd 3986 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π¦ β dom β‘(π§ β π β¦ (π΄(+gβπΊ)π§))) |
96 | | funimass3 7005 |
. . . . . . . . . 10
β’ ((Fun
β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β§ π¦ β dom β‘(π§ β π β¦ (π΄(+gβπΊ)π§))) β ((β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π β π¦ β (β‘β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π))) |
97 | 92, 95, 96 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β ((β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π¦) β π β π¦ β (β‘β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π))) |
98 | 80, 97 | mpbid 231 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π¦ β (β‘β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
99 | 41 | adantr 482 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β [π΄] βΌ = ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
100 | | imacnvcnv 6159 |
. . . . . . . . 9
β’ (β‘β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π) = ((π§ β π β¦ (π΄(+gβπΊ)π§)) β π) |
101 | 99, 100 | eqtr4di 2791 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β [π΄] βΌ = (β‘β‘(π§ β π β¦ (π΄(+gβπΊ)π§)) β π)) |
102 | 98, 101 | sseqtrrd 3986 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π΄ β π) β§ (π¦ β π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) β π¦ β [π΄] βΌ ) |
103 | 102 | expr 458 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π΄ β π) β§ π¦ β π) β ((π΄ β π¦ β§ (π½ βΎt π¦) β Conn) β π¦ β [π΄] βΌ )) |
104 | 58, 103 | sylan2 594 |
. . . . 5
β’ (((πΊ β TopGrp β§ π΄ β π) β§ π¦ β π« π) β ((π΄ β π¦ β§ (π½ βΎt π¦) β Conn) β π¦ β [π΄] βΌ )) |
105 | 104 | ralrimiva 3140 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β βπ¦ β π« π((π΄ β π¦ β§ (π½ βΎt π¦) β Conn) β π¦ β [π΄] βΌ )) |
106 | | eleq2w 2818 |
. . . . . 6
β’ (π₯ = π¦ β (π΄ β π₯ β π΄ β π¦)) |
107 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π¦ β (π½ βΎt π₯) = (π½ βΎt π¦)) |
108 | 107 | eleq1d 2819 |
. . . . . 6
β’ (π₯ = π¦ β ((π½ βΎt π₯) β Conn β (π½ βΎt π¦) β Conn)) |
109 | 106, 108 | anbi12d 632 |
. . . . 5
β’ (π₯ = π¦ β ((π΄ β π₯ β§ (π½ βΎt π₯) β Conn) β (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) |
110 | 109 | ralrab 3652 |
. . . 4
β’
(βπ¦ β
{π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦ β [π΄] βΌ β
βπ¦ β π«
π((π΄ β π¦ β§ (π½ βΎt π¦) β Conn) β π¦ β [π΄] βΌ )) |
111 | 105, 110 | sylibr 233 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β βπ¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦ β [π΄] βΌ ) |
112 | | unissb 4901 |
. . 3
β’ (βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β [π΄] βΌ β
βπ¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦ β [π΄] βΌ ) |
113 | 111, 112 | sylibr 233 |
. 2
β’ ((πΊ β TopGrp β§ π΄ β π) β βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β [π΄] βΌ ) |
114 | 57, 113 | eqssd 3962 |
1
β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) |