Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β πΊ β TopGrp) |
2 | | subgntr.h |
. . . . . . . . 9
β’ π½ = (TopOpenβπΊ) |
3 | | cldsubg.2 |
. . . . . . . . 9
β’ π = (BaseβπΊ) |
4 | 2, 3 | tgptopon 23456 |
. . . . . . . 8
β’ (πΊ β TopGrp β π½ β (TopOnβπ)) |
5 | 1, 4 | syl 17 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π½ β (TopOnβπ)) |
6 | | toponuni 22286 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π = βͺ π½) |
8 | 7 | difeq1d 4085 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π β βͺ
((π / π
) β {π})) = (βͺ π½ β βͺ ((π
/ π
) β {π}))) |
9 | | simpl2 1193 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π β (SubGrpβπΊ)) |
10 | | unisng 4890 |
. . . . . . . . 9
β’ (π β (SubGrpβπΊ) β βͺ {π}
= π) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
{π} = π) |
12 | 11 | uneq2d 4127 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
((π / π
) β {π}) βͺ βͺ {π}) = (βͺ ((π
/ π
) β {π}) βͺ π)) |
13 | | uniun 4895 |
. . . . . . . 8
β’ βͺ (((π
/ π
) β {π}) βͺ {π}) = (βͺ ((π / π
) β {π}) βͺ βͺ {π}) |
14 | | undif1 4439 |
. . . . . . . . . . 11
β’ (((π / π
) β {π}) βͺ {π}) = ((π / π
) βͺ {π}) |
15 | | cldsubg.1 |
. . . . . . . . . . . . . . . 16
β’ π
= (πΊ ~QG π) |
16 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0gβπΊ) = (0gβπΊ) |
17 | 3, 15, 16 | eqgid 18990 |
. . . . . . . . . . . . . . 15
β’ (π β (SubGrpβπΊ) β
[(0gβπΊ)]π
= π) |
18 | 9, 17 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β [(0gβπΊ)]π
= π) |
19 | 15 | ovexi 7395 |
. . . . . . . . . . . . . . 15
β’ π
β V |
20 | | tgpgrp 23452 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β TopGrp β πΊ β Grp) |
21 | 1, 20 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β πΊ β Grp) |
22 | 3, 16 | grpidcl 18786 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β Grp β
(0gβπΊ)
β π) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (0gβπΊ) β π) |
24 | | ecelqsg 8717 |
. . . . . . . . . . . . . . 15
β’ ((π
β V β§
(0gβπΊ)
β π) β
[(0gβπΊ)]π
β (π / π
)) |
25 | 19, 23, 24 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β [(0gβπΊ)]π
β (π / π
)) |
26 | 18, 25 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π β (π / π
)) |
27 | 26 | snssd 4773 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β {π} β (π / π
)) |
28 | | ssequn2 4147 |
. . . . . . . . . . . 12
β’ ({π} β (π / π
) β ((π / π
) βͺ {π}) = (π / π
)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((π / π
) βͺ {π}) = (π / π
)) |
30 | 14, 29 | eqtrid 2785 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (((π / π
) β {π}) βͺ {π}) = (π / π
)) |
31 | 30 | unieqd 4883 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
(((π / π
) β {π}) βͺ {π}) = βͺ (π / π
)) |
32 | 3, 15 | eqger 18988 |
. . . . . . . . . . 11
β’ (π β (SubGrpβπΊ) β π
Er π) |
33 | 9, 32 | syl 17 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π
Er π) |
34 | 19 | a1i 11 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π
β V) |
35 | 33, 34 | uniqs2 8724 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
(π / π
) = π) |
36 | 31, 35 | eqtrd 2773 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
(((π / π
) β {π}) βͺ {π}) = π) |
37 | 13, 36 | eqtr3id 2787 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
((π / π
) β {π}) βͺ βͺ {π}) = π) |
38 | 12, 37 | eqtr3d 2775 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
((π / π
) β {π}) βͺ π) = π) |
39 | | difss 4095 |
. . . . . . . . 9
β’ ((π / π
) β {π}) β (π / π
) |
40 | 39 | unissi 4878 |
. . . . . . . 8
β’ βͺ ((π
/ π
) β {π}) β βͺ (π
/ π
) |
41 | 40, 35 | sseqtrid 4000 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
((π / π
) β {π}) β π) |
42 | | df-ne 2941 |
. . . . . . . . . . . . 13
β’ (π₯ β π β Β¬ π₯ = π) |
43 | 33 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β π
Er π) |
44 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β π₯ β (π / π
)) |
45 | 26 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β π β (π / π
)) |
46 | 43, 44, 45 | qsdisj 8739 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β (π₯ = π β¨ (π₯ β© π) = β
)) |
47 | 46 | ord 863 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β (Β¬ π₯ = π β (π₯ β© π) = β
)) |
48 | | disj2 4421 |
. . . . . . . . . . . . . 14
β’ ((π₯ β© π) = β
β π₯ β (V β π)) |
49 | 47, 48 | syl6ib 251 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β (Β¬ π₯ = π β π₯ β (V β π))) |
50 | 42, 49 | biimtrid 241 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π₯ β (π / π
)) β (π₯ β π β π₯ β (V β π))) |
51 | 50 | expimpd 455 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((π₯ β (π / π
) β§ π₯ β π) β π₯ β (V β π))) |
52 | | eldifsn 4751 |
. . . . . . . . . . 11
β’ (π₯ β ((π / π
) β {π}) β (π₯ β (π / π
) β§ π₯ β π)) |
53 | | velpw 4569 |
. . . . . . . . . . 11
β’ (π₯ β π« (V β
π) β π₯ β (V β π)) |
54 | 51, 52, 53 | 3imtr4g 296 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π₯ β ((π / π
) β {π}) β π₯ β π« (V β π))) |
55 | 54 | ssrdv 3954 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((π / π
) β {π}) β π« (V β π)) |
56 | | sspwuni 5064 |
. . . . . . . . 9
β’ (((π / π
) β {π}) β π« (V β π) β βͺ ((π
/ π
) β {π}) β (V β π)) |
57 | 55, 56 | sylib 217 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
((π / π
) β {π}) β (V β π)) |
58 | | disj2 4421 |
. . . . . . . 8
β’ ((βͺ ((π
/ π
) β {π}) β© π) = β
β βͺ ((π
/ π
) β {π}) β (V β π)) |
59 | 57, 58 | sylibr 233 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
((π / π
) β {π}) β© π) = β
) |
60 | | uneqdifeq 4454 |
. . . . . . 7
β’ ((βͺ ((π
/ π
) β {π}) β π β§ (βͺ ((π / π
) β {π}) β© π) = β
) β ((βͺ ((π
/ π
) β {π}) βͺ π) = π β (π β βͺ
((π / π
) β {π})) = π)) |
61 | 41, 59, 60 | syl2anc 585 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((βͺ
((π / π
) β {π}) βͺ π) = π β (π β βͺ
((π / π
) β {π})) = π)) |
62 | 38, 61 | mpbid 231 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π β βͺ
((π / π
) β {π})) = π) |
63 | 8, 62 | eqtr3d 2775 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
π½ β βͺ ((π
/ π
) β {π})) = π) |
64 | | topontop 22285 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
65 | 5, 64 | syl 17 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π½ β Top) |
66 | | simpl3 1194 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π / π
) β Fin) |
67 | | diffi 9129 |
. . . . . . 7
β’ ((π / π
) β Fin β ((π / π
) β {π}) β Fin) |
68 | 66, 67 | syl 17 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((π / π
) β {π}) β Fin) |
69 | | vex 3451 |
. . . . . . . . . 10
β’ π₯ β V |
70 | 69 | elqs 8714 |
. . . . . . . . 9
β’ (π₯ β (π / π
) β βπ¦ β π π₯ = [π¦]π
) |
71 | | simpll2 1214 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β π β (SubGrpβπΊ)) |
72 | | subgrcl 18941 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β πΊ β Grp) |
74 | 3 | subgss 18937 |
. . . . . . . . . . . . . . 15
β’ (π β (SubGrpβπΊ) β π β π) |
75 | 9, 74 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π β π) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β π β π) |
77 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β π¦ β π) |
78 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
79 | 3, 15, 78 | eqglact 18989 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ π β π β§ π¦ β π) β [π¦]π
= ((π§ β π β¦ (π¦(+gβπΊ)π§)) β π)) |
80 | 73, 76, 77, 79 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β [π¦]π
= ((π§ β π β¦ (π¦(+gβπΊ)π§)) β π)) |
81 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β π β (Clsdβπ½)) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β¦ (π¦(+gβπΊ)π§)) = (π§ β π β¦ (π¦(+gβπΊ)π§)) |
83 | 82, 3, 78, 2 | tgplacthmeo 23477 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(+gβπΊ)π§)) β (π½Homeoπ½)) |
84 | 1, 83 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β (π§ β π β¦ (π¦(+gβπΊ)π§)) β (π½Homeoπ½)) |
85 | 75, 7 | sseqtrd 3988 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π β βͺ π½) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β π β βͺ π½) |
87 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ βͺ π½ =
βͺ π½ |
88 | 87 | hmeocld 23141 |
. . . . . . . . . . . . . 14
β’ (((π§ β π β¦ (π¦(+gβπΊ)π§)) β (π½Homeoπ½) β§ π β βͺ π½) β (π β (Clsdβπ½) β ((π§ β π β¦ (π¦(+gβπΊ)π§)) β π) β (Clsdβπ½))) |
89 | 84, 86, 88 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β (π β (Clsdβπ½) β ((π§ β π β¦ (π¦(+gβπΊ)π§)) β π) β (Clsdβπ½))) |
90 | 81, 89 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β ((π§ β π β¦ (π¦(+gβπΊ)π§)) β π) β (Clsdβπ½)) |
91 | 80, 90 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β [π¦]π
β (Clsdβπ½)) |
92 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π₯ = [π¦]π
β (π₯ β (Clsdβπ½) β [π¦]π
β (Clsdβπ½))) |
93 | 91, 92 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β§ π¦ β π) β (π₯ = [π¦]π
β π₯ β (Clsdβπ½))) |
94 | 93 | rexlimdva 3149 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βπ¦ β π π₯ = [π¦]π
β π₯ β (Clsdβπ½))) |
95 | 70, 94 | biimtrid 241 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π₯ β (π / π
) β π₯ β (Clsdβπ½))) |
96 | 95 | ssrdv 3954 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (π / π
) β (Clsdβπ½)) |
97 | 96 | ssdifssd 4106 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β ((π / π
) β {π}) β (Clsdβπ½)) |
98 | 87 | unicld 22420 |
. . . . . 6
β’ ((π½ β Top β§ ((π / π
) β {π}) β Fin β§ ((π / π
) β {π}) β (Clsdβπ½)) β βͺ
((π / π
) β {π}) β (Clsdβπ½)) |
99 | 65, 68, 97, 98 | syl3anc 1372 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β βͺ
((π / π
) β {π}) β (Clsdβπ½)) |
100 | 87 | cldopn 22405 |
. . . . 5
β’ (βͺ ((π
/ π
) β {π}) β (Clsdβπ½) β (βͺ π½
β βͺ ((π / π
) β {π})) β π½) |
101 | 99, 100 | syl 17 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β (βͺ
π½ β βͺ ((π
/ π
) β {π})) β π½) |
102 | 63, 101 | eqeltrrd 2835 |
. . 3
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β§ π β (Clsdβπ½)) β π β π½) |
103 | 102 | ex 414 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β (π β (Clsdβπ½) β π β π½)) |
104 | 2 | opnsubg 23482 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π β π½) β π β (Clsdβπ½)) |
105 | 104 | 3expia 1122 |
. . 3
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π β π½ β π β (Clsdβπ½))) |
106 | 105 | 3adant3 1133 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β (π β π½ β π β (Clsdβπ½))) |
107 | 103, 106 | impbid 211 |
1
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π
) β Fin) β (π β (Clsdβπ½) β π β π½)) |