Step | Hyp | Ref
| Expression |
1 | | simpl1 1011 |
. . . . . . . 8
   SubGrp              |
2 | | subgntr.h |
. . . . . . . . 9
     |
3 | | cldsubg.2 |
. . . . . . . . 9
     |
4 | 2, 3 | tgptopon 21097 |
. . . . . . . 8
 TopOn    |
5 | 1, 4 | syl 17 |
. . . . . . 7
   SubGrp            TopOn    |
6 | | toponuni 19942 |
. . . . . . 7
 TopOn 
   |
7 | 5, 6 | syl 17 |
. . . . . 6
   SubGrp               |
8 | 7 | difeq1d 3550 |
. . . . 5
   SubGrp                                     |
9 | | simpl2 1012 |
. . . . . . . . 9
   SubGrp            SubGrp    |
10 | | unisng 4214 |
. . . . . . . . 9
 SubGrp 
  
  |
11 | 9, 10 | syl 17 |
. . . . . . . 8
   SubGrp              
  |
12 | 11 | uneq2d 3588 |
. . . . . . 7
   SubGrp                                       |
13 | | uniun 4217 |
. . . . . . . 8
                            |
14 | | undif1 3842 |
. . . . . . . . . . 11
     
               |
15 | | cldsubg.1 |
. . . . . . . . . . . . . . . 16

~QG   |
16 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
         |
17 | 3, 15, 16 | eqgid 16869 |
. . . . . . . . . . . . . . 15
 SubGrp 
      ![] ]](rbrack.gif)   |
18 | 9, 17 | syl 17 |
. . . . . . . . . . . . . 14
   SubGrp                  ![] ]](rbrack.gif)   |
19 | | ovex 6318 |
. . . . . . . . . . . . . . . 16
 ~QG   |
20 | 15, 19 | eqeltri 2525 |
. . . . . . . . . . . . . . 15
 |
21 | | tgpgrp 21093 |
. . . . . . . . . . . . . . . . 17
   |
22 | 1, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
   SubGrp              |
23 | 3, 16 | grpidcl 16694 |
. . . . . . . . . . . . . . . 16
       |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
   SubGrp                  |
25 | | ecelqsg 7418 |
. . . . . . . . . . . . . . 15
             ![] ]](rbrack.gif)       |
26 | 20, 24, 25 | sylancr 669 |
. . . . . . . . . . . . . 14
   SubGrp                  ![] ]](rbrack.gif)       |
27 | 18, 26 | eqeltrrd 2530 |
. . . . . . . . . . . . 13
   SubGrp                  |
28 | 27 | snssd 4117 |
. . . . . . . . . . . 12
   SubGrp                    |
29 | | ssequn2 3607 |
. . . . . . . . . . . 12
      
              |
30 | 28, 29 | sylib 200 |
. . . . . . . . . . 11
   SubGrp                          |
31 | 14, 30 | syl5eq 2497 |
. . . . . . . . . 10
   SubGrp                              |
32 | 31 | unieqd 4208 |
. . . . . . . . 9
   SubGrp                                |
33 | 3, 15 | eqger 16867 |
. . . . . . . . . . 11
 SubGrp 
  |
34 | 9, 33 | syl 17 |
. . . . . . . . . 10
   SubGrp              |
35 | 20 | a1i 11 |
. . . . . . . . . 10
   SubGrp              |
36 | 34, 35 | uniqs2 7425 |
. . . . . . . . 9
   SubGrp                   |
37 | 32, 36 | eqtrd 2485 |
. . . . . . . 8
   SubGrp                           |
38 | 13, 37 | syl5eqr 2499 |
. . . . . . 7
   SubGrp                            |
39 | 12, 38 | eqtr3d 2487 |
. . . . . 6
   SubGrp                         |
40 | | difss 3560 |
. . . . . . . . 9
       
     |
41 | 40 | unissi 4221 |
. . . . . . . 8
     
         |
42 | 41, 36 | syl5sseq 3480 |
. . . . . . 7
   SubGrp                 
     |
43 | | df-ne 2624 |
. . . . . . . . . . . . 13

  |
44 | 34 | adantr 467 |
. . . . . . . . . . . . . . . 16
    SubGrp                   |
45 | | simpr 463 |
. . . . . . . . . . . . . . . 16
    SubGrp                       |
46 | 27 | adantr 467 |
. . . . . . . . . . . . . . . 16
    SubGrp                       |
47 | 44, 45, 46 | qsdisj 7440 |
. . . . . . . . . . . . . . 15
    SubGrp                  
    |
48 | 47 | ord 379 |
. . . . . . . . . . . . . 14
    SubGrp                 
     |
49 | | disj2 3812 |
. . . . . . . . . . . . . 14
  
    |
50 | 48, 49 | syl6ib 230 |
. . . . . . . . . . . . 13
    SubGrp                 
     |
51 | 43, 50 | syl5bi 221 |
. . . . . . . . . . . 12
    SubGrp                       |
52 | 51 | expimpd 608 |
. . . . . . . . . . 11
   SubGrp                  
     |
53 | | eldifsn 4097 |
. . . . . . . . . . 11
        
    
   |
54 | | selpw 3958 |
. . . . . . . . . . 11
   
    |
55 | 52, 53, 54 | 3imtr4g 274 |
. . . . . . . . . 10
   SubGrp                    
      |
56 | 55 | ssrdv 3438 |
. . . . . . . . 9
   SubGrp                
    
   |
57 | | sspwuni 4367 |
. . . . . . . . 9
     
    
              |
58 | 56, 57 | sylib 200 |
. . . . . . . 8
   SubGrp                 
       |
59 | | disj2 3812 |
. . . . . . . 8
                         |
60 | 58, 59 | sylibr 216 |
. . . . . . 7
   SubGrp                         |
61 | | uneqdifeq 3856 |
. . . . . . 7
                 
            
   
              |
62 | 42, 60, 61 | syl2anc 667 |
. . . . . 6
   SubGrp                       
              |
63 | 39, 62 | mpbid 214 |
. . . . 5
   SubGrp                         |
64 | 8, 63 | eqtr3d 2487 |
. . . 4
   SubGrp             
     
      |
65 | | topontop 19941 |
. . . . . . 7
 TopOn 
  |
66 | 5, 65 | syl 17 |
. . . . . 6
   SubGrp              |
67 | | simpl3 1013 |
. . . . . . 7
   SubGrp                  |
68 | | diffi 7803 |
. . . . . . 7
         
     |
69 | 67, 68 | syl 17 |
. . . . . 6
   SubGrp                
     |
70 | | vex 3048 |
. . . . . . . . . 10
 |
71 | 70 | elqs 7416 |
. . . . . . . . 9
    

  ![] ]](rbrack.gif)   |
72 | | simpll2 1048 |
. . . . . . . . . . . . . 14
    SubGrp             SubGrp    |
73 | | subgrcl 16822 |
. . . . . . . . . . . . . 14
 SubGrp 
  |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
    SubGrp               |
75 | 3 | subgss 16818 |
. . . . . . . . . . . . . . 15
 SubGrp 
  |
76 | 9, 75 | syl 17 |
. . . . . . . . . . . . . 14
   SubGrp              |
77 | 76 | adantr 467 |
. . . . . . . . . . . . 13
    SubGrp               |
78 | | simpr 463 |
. . . . . . . . . . . . 13
    SubGrp               |
79 | | eqid 2451 |
. . . . . . . . . . . . . 14
       |
80 | 3, 15, 79 | eqglact 16868 |
. . . . . . . . . . . . 13
     ![] ]](rbrack.gif)                |
81 | 74, 77, 78, 80 | syl3anc 1268 |
. . . . . . . . . . . 12
    SubGrp               ![] ]](rbrack.gif)                |
82 | | simplr 762 |
. . . . . . . . . . . . 13
    SubGrp                   |
83 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
                   |
84 | 83, 3, 79, 2 | tgplacthmeo 21118 |
. . . . . . . . . . . . . . 15
                  |
85 | 1, 84 | sylan 474 |
. . . . . . . . . . . . . 14
    SubGrp                            |
86 | 76, 7 | sseqtrd 3468 |
. . . . . . . . . . . . . . 15
   SubGrp               |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . 14
    SubGrp                |
88 | | eqid 2451 |
. . . . . . . . . . . . . . 15
   |
89 | 88 | hmeocld 20782 |
. . . . . . . . . . . . . 14
                                          |
90 | 85, 87, 89 | syl2anc 667 |
. . . . . . . . . . . . 13
    SubGrp             
   
                    |
91 | 82, 90 | mpbid 214 |
. . . . . . . . . . . 12
    SubGrp                                |
92 | 81, 91 | eqeltrd 2529 |
. . . . . . . . . . 11
    SubGrp               ![] ]](rbrack.gif)       |
93 | | eleq1 2517 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)
       ![] ]](rbrack.gif)        |
94 | 92, 93 | syl5ibrcom 226 |
. . . . . . . . . 10
    SubGrp                ![] ]](rbrack.gif)        |
95 | 94 | rexlimdva 2879 |
. . . . . . . . 9
   SubGrp             
  ![] ]](rbrack.gif)
       |
96 | 71, 95 | syl5bi 221 |
. . . . . . . 8
   SubGrp                
       |
97 | 96 | ssrdv 3438 |
. . . . . . 7
   SubGrp                      |
98 | 97 | ssdifssd 3571 |
. . . . . 6
   SubGrp                
         |
99 | 88 | unicld 20061 |
. . . . . 6
                                      |
100 | 66, 69, 98, 99 | syl3anc 1268 |
. . . . 5
   SubGrp                 
         |
101 | 88 | cldopn 20046 |
. . . . 5
                            |
102 | 100, 101 | syl 17 |
. . . 4
   SubGrp             
     
      |
103 | 64, 102 | eqeltrrd 2530 |
. . 3
   SubGrp              |
104 | 103 | ex 436 |
. 2
  SubGrp               |
105 | 2 | opnsubg 21122 |
. . . 4
  SubGrp 

      |
106 | 105 | 3expia 1210 |
. . 3
  SubGrp  

       |
107 | 106 | 3adant3 1028 |
. 2
  SubGrp               |
108 | 104, 107 | impbid 194 |
1
  SubGrp               |