Step | Hyp | Ref
| Expression |
1 | | sylow1.g |
. . 3
   |
2 | | sylow1lem.s |
. . . 4
 
          |
3 | | sylow1.x |
. . . . . 6
     |
4 | | fvex 5880 |
. . . . . 6
     |
5 | 3, 4 | eqeltri 2527 |
. . . . 5
 |
6 | 5 | pwex 4589 |
. . . 4
  |
7 | 2, 6 | rabex2 4559 |
. . 3
 |
8 | 1, 7 | jctir 541 |
. 2
     |
9 | 1 | adantr 467 |
. . . . . . . . . . . 12
 

 
  |
10 | | simprl 765 |
. . . . . . . . . . . 12
 

 
  |
11 | | sylow1lem.a |
. . . . . . . . . . . . 13
    |
12 | | eqid 2453 |
. . . . . . . . . . . . 13
         |
13 | 3, 11, 12 | grplmulf1o 16740 |
. . . . . . . . . . . 12
 
           |
14 | 9, 10, 13 | syl2anc 667 |
. . . . . . . . . . 11
 

            |
15 | | f1of1 5818 |
. . . . . . . . . . 11
                   |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
 

            |
17 | | simprr 767 |
. . . . . . . . . . . . 13
 

    |
18 | | fveq2 5870 |
. . . . . . . . . . . . . . 15
           |
19 | 18 | eqeq1d 2455 |
. . . . . . . . . . . . . 14
         
           |
20 | 19, 2 | elrab2 3200 |
. . . . . . . . . . . . 13

             |
21 | 17, 20 | sylib 200 |
. . . . . . . . . . . 12
 

               |
22 | 21 | simpld 461 |
. . . . . . . . . . 11
 

     |
23 | 22 | elpwid 3963 |
. . . . . . . . . 10
 

 
  |
24 | | f1ssres 5791 |
. . . . . . . . . 10
          
    
       |
25 | 16, 23, 24 | syl2anc 667 |
. . . . . . . . 9
 

              |
26 | | resmpt 5157 |
. . . . . . . . . 10
             |
27 | | f1eq1 5779 |
. . . . . . . . . 10
                
    

          |
28 | 23, 26, 27 | 3syl 18 |
. . . . . . . . 9
 

                        |
29 | 25, 28 | mpbid 214 |
. . . . . . . 8
 

            |
30 | | f1f 5784 |
. . . . . . . 8
                   |
31 | | frn 5740 |
. . . . . . . 8
        

     |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
 

        |
33 | 5 | elpw2 4570 |
. . . . . . 7
            |
34 | 32, 33 | sylibr 216 |
. . . . . 6
 

         |
35 | | f1f1orn 5830 |
. . . . . . . . 9
                       |
36 | | vex 3050 |
. . . . . . . . . 10
 |
37 | 36 | f1oen 7595 |
. . . . . . . . 9
            
      |
38 | 29, 35, 37 | 3syl 18 |
. . . . . . . 8
 

 
      |
39 | | sylow1.f |
. . . . . . . . . . 11
   |
40 | 39 | adantr 467 |
. . . . . . . . . 10
 

 
  |
41 | | ssfi 7797 |
. . . . . . . . . 10
     |
42 | 40, 23, 41 | syl2anc 667 |
. . . . . . . . 9
 

    |
43 | | ssfi 7797 |
. . . . . . . . . 10
      
      |
44 | 40, 32, 43 | syl2anc 667 |
. . . . . . . . 9
 

        |
45 | | hashen 12537 |
. . . . . . . . 9
                           |
46 | 42, 44, 45 | syl2anc 667 |
. . . . . . . 8
 

              
       |
47 | 38, 46 | mpbird 236 |
. . . . . . 7
 

                |
48 | 21 | simprd 465 |
. . . . . . 7
 

            |
49 | 47, 48 | eqtr3d 2489 |
. . . . . 6
 

                |
50 | | fveq2 5870 |
. . . . . . . 8
                   |
51 | 50 | eqeq1d 2455 |
. . . . . . 7
                             |
52 | 51, 2 | elrab2 3200 |
. . . . . 6
             

           |
53 | 34, 49, 52 | sylanbrc 671 |
. . . . 5
 

        |
54 | 53 | ralrimivva 2811 |
. . . 4
  
      |
55 | | sylow1lem.m |
. . . . 5
        |
56 | 55 | fmpt2 6865 |
. . . 4
 

           |
57 | 54, 56 | sylib 200 |
. . 3
        |
58 | 1 | adantr 467 |
. . . . . . . 8
 
   |
59 | | eqid 2453 |
. . . . . . . . 9
         |
60 | 3, 59 | grpidcl 16706 |
. . . . . . . 8
       |
61 | 58, 60 | syl 17 |
. . . . . . 7
 
       |
62 | | simpr 463 |
. . . . . . 7
 
   |
63 | | simpr 463 |
. . . . . . . . . 10
     
   |
64 | | simpl 459 |
. . . . . . . . . . 11
     
       |
65 | 64 | oveq1d 6310 |
. . . . . . . . . 10
     
           |
66 | 63, 65 | mpteq12dv 4484 |
. . . . . . . . 9
     
          
    |
67 | 66 | rneqd 5065 |
. . . . . . . 8
     
               |
68 | | vex 3050 |
. . . . . . . . . 10
 |
69 | 68 | mptex 6141 |
. . . . . . . . 9
         |
70 | 69 | rnex 6732 |
. . . . . . . 8
     
   |
71 | 67, 55, 70 | ovmpt2a 6432 |
. . . . . . 7
     
                 |
72 | 61, 62, 71 | syl2anc 667 |
. . . . . 6
 
                 |
73 | | ssrab2 3516 |
. . . . . . . . . . . . . . 15
             |
74 | 2, 73 | eqsstri 3464 |
. . . . . . . . . . . . . 14
  |
75 | 74, 62 | sseldi 3432 |
. . . . . . . . . . . . 13
 
    |
76 | 75 | elpwid 3963 |
. . . . . . . . . . . 12
 
   |
77 | 76 | sselda 3434 |
. . . . . . . . . . 11
       |
78 | 3, 11, 59 | grplid 16708 |
. . . . . . . . . . . 12
 
         |
79 | 58, 78 | sylan 474 |
. . . . . . . . . . 11
         
   |
80 | 77, 79 | syldan 473 |
. . . . . . . . . 10
         
   |
81 | 80 | mpteq2dva 4492 |
. . . . . . . . 9
 
      
      |
82 | | mptresid 5162 |
. . . . . . . . 9
    |
83 | 81, 82 | syl6eq 2503 |
. . . . . . . 8
 
      
     |
84 | 83 | rneqd 5065 |
. . . . . . 7
 
        
   |
85 | | rnresi 5184 |
. . . . . . 7
  |
86 | 84, 85 | syl6eq 2503 |
. . . . . 6
 
           |
87 | 72, 86 | eqtrd 2487 |
. . . . 5
 
         |
88 | | ovex 6323 |
. . . . . . . . . 10
   |
89 | | oveq2 6303 |
. . . . . . . . . 10
   
       |
90 | 88, 89 | abrexco 6154 |
. . . . . . . . 9
   
        
 
    |
91 | | simprr 767 |
. . . . . . . . . . . . 13
    
 
  |
92 | 62 | adantr 467 |
. . . . . . . . . . . . 13
    
 
  |
93 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
   |
94 | | simpl 459 |
. . . . . . . . . . . . . . . . 17
 
   |
95 | 94 | oveq1d 6310 |
. . . . . . . . . . . . . . . 16
 
       |
96 | 93, 95 | mpteq12dv 4484 |
. . . . . . . . . . . . . . 15
 
           |
97 | 96 | rneqd 5065 |
. . . . . . . . . . . . . 14
 
           |
98 | 68 | mptex 6141 |
. . . . . . . . . . . . . . 15
     |
99 | 98 | rnex 6732 |
. . . . . . . . . . . . . 14
     |
100 | 97, 55, 99 | ovmpt2a 6432 |
. . . . . . . . . . . . 13
 
         |
101 | 91, 92, 100 | syl2anc 667 |
. . . . . . . . . . . 12
    
 
        |
102 | | eqid 2453 |
. . . . . . . . . . . . 13
         |
103 | 102 | rnmpt 5083 |
. . . . . . . . . . . 12
          |
104 | 101, 103 | syl6eq 2503 |
. . . . . . . . . . 11
    
 
   
     |
105 | 104 | rexeqdv 2996 |
. . . . . . . . . 10
    
 
 
       
         |
106 | 105 | abbidv 2571 |
. . . . . . . . 9
    
 
  
        
         |
107 | 58 | ad2antrr 733 |
. . . . . . . . . . . . 13
   
 
     |
108 | | simprl 765 |
. . . . . . . . . . . . . 14
    
 
  |
109 | 108 | adantr 467 |
. . . . . . . . . . . . 13
   
 
     |
110 | 91 | adantr 467 |
. . . . . . . . . . . . 13
   
 
     |
111 | 77 | adantlr 722 |
. . . . . . . . . . . . 13
   
 
     |
112 | 3, 11 | grpass 16692 |
. . . . . . . . . . . . 13
  
    
       |
113 | 107, 109,
110, 111, 112 | syl13anc 1271 |
. . . . . . . . . . . 12
   
 
     
       |
114 | 113 | eqeq2d 2463 |
. . . . . . . . . . 11
   
 
       
 
     |
115 | 114 | rexbidva 2900 |
. . . . . . . . . 10
    
 
 
   

 
     |
116 | 115 | abbidv 2571 |
. . . . . . . . 9
    
 
                |
117 | 90, 106, 116 | 3eqtr4a 2513 |
. . . . . . . 8
    
 
  
              |
118 | | eqid 2453 |
. . . . . . . . 9
       
     |
119 | 118 | rnmpt 5083 |
. . . . . . . 8
        
      |
120 | | eqid 2453 |
. . . . . . . . 9
             |
121 | 120 | rnmpt 5083 |
. . . . . . . 8
   
          |
122 | 117, 119,
121 | 3eqtr4g 2512 |
. . . . . . 7
    
 
              |
123 | 57 | ad2antrr 733 |
. . . . . . . . 9
    
 
       |
124 | 123, 91, 92 | fovrnd 6446 |
. . . . . . . 8
    
 
    |
125 | | simpr 463 |
. . . . . . . . . . . 12
 
       |
126 | | simpl 459 |
. . . . . . . . . . . . 13
 
  
  |
127 | 126 | oveq1d 6310 |
. . . . . . . . . . . 12
 
         |
128 | 125, 127 | mpteq12dv 4484 |
. . . . . . . . . . 11
 
               |
129 | | oveq2 6303 |
. . . . . . . . . . . 12
 
     |
130 | 129 | cbvmptv 4498 |
. . . . . . . . . . 11
       
     |
131 | 128, 130 | syl6eq 2503 |
. . . . . . . . . 10
 
               |
132 | 131 | rneqd 5065 |
. . . . . . . . 9
 
       
       |
133 | | ovex 6323 |
. . . . . . . . . . 11
   |
134 | 133 | mptex 6141 |
. . . . . . . . . 10
       |
135 | 134 | rnex 6732 |
. . . . . . . . 9
       |
136 | 132, 55, 135 | ovmpt2a 6432 |
. . . . . . . 8
                 |
137 | 108, 124,
136 | syl2anc 667 |
. . . . . . 7
    
 
            |
138 | 1 | ad2antrr 733 |
. . . . . . . . 9
    
 
  |
139 | 3, 11 | grpcl 16691 |
. . . . . . . . 9
 
     |
140 | 138, 108,
91, 139 | syl3anc 1269 |
. . . . . . . 8
    
 
    |
141 | | simpr 463 |
. . . . . . . . . . 11
   
   |
142 | | simpl 459 |
. . . . . . . . . . . 12
   
     |
143 | 142 | oveq1d 6310 |
. . . . . . . . . . 11
   
         |
144 | 141, 143 | mpteq12dv 4484 |
. . . . . . . . . 10
   
        
    |
145 | 144 | rneqd 5065 |
. . . . . . . . 9
   
             |
146 | 68 | mptex 6141 |
. . . . . . . . . 10
       |
147 | 146 | rnex 6732 |
. . . . . . . . 9
   
   |
148 | 145, 55, 147 | ovmpt2a 6432 |
. . . . . . . 8
   
             |
149 | 140, 92, 148 | syl2anc 667 |
. . . . . . 7
    
 
 
          |
150 | 122, 137,
149 | 3eqtr4rd 2498 |
. . . . . 6
    
 
 
  
     |
151 | 150 | ralrimivva 2811 |
. . . . 5
 
 

 
  
     |
152 | 87, 151 | jca 535 |
. . . 4
 
        

           |
153 | 152 | ralrimiva 2804 |
. . 3
          
           |
154 | 57, 153 | jca 535 |
. 2

             

 
  
       |
155 | 3, 11, 59 | isga 16957 |
. 2
   

             

             |
156 | 8, 154, 155 | sylanbrc 671 |
1

    |