Proof of Theorem psgnunilem1
Step | Hyp | Ref
| Expression |
1 | | psgnunilem1.q |
. . . . . . . 8
   |
2 | | eqid 2452 |
. . . . . . . . 9
pmTrsp  pmTrsp   |
3 | | psgnunilem1.t |
. . . . . . . . 9
pmTrsp   |
4 | 2, 3 | pmtrfinv 17113 |
. . . . . . . 8
 

   |
5 | 1, 4 | syl 17 |
. . . . . . 7
      |
6 | | coeq1 4970 |
. . . . . . . 8
 
     |
7 | 6 | eqeq1d 2454 |
. . . . . . 7
    
 
    |
8 | 5, 7 | syl5ibrcom 230 |
. . . . . 6
   
    |
9 | 8 | adantr 471 |
. . . . 5
 
  
      |
10 | 9 | imp 435 |
. . . 4
      

   |
11 | 10 | orcd 398 |
. . 3
          

    

     |
12 | | psgnunilem1.p |
. . . . . . . . . 10
   |
13 | 2, 3 | pmtrfcnv 17116 |
. . . . . . . . . 10
 
  |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
 
  |
15 | 14 | eqcomd 2458 |
. . . . . . . 8
    |
16 | 15 | coeq2d 4975 |
. . . . . . 7
            |
17 | 2, 3 | pmtrff1o 17115 |
. . . . . . . . 9
       |
18 | 12, 17 | syl 17 |
. . . . . . . 8
       |
19 | 2, 3 | pmtrfconj 17118 |
. . . . . . . 8
              |
20 | 1, 18, 19 | syl2anc 671 |
. . . . . . 7
        |
21 | 16, 20 | eqeltrd 2530 |
. . . . . 6
       |
22 | 21 | ad2antrr 737 |
. . . . 5
            |
23 | 12 | ad2antrr 737 |
. . . . 5
        |
24 | | coass 5333 |
. . . . . . 7
         
   |
25 | 2, 3 | pmtrfinv 17113 |
. . . . . . . . . 10
 

   |
26 | 12, 25 | syl 17 |
. . . . . . . . 9
      |
27 | 26 | coeq2d 4975 |
. . . . . . . 8
    
         |
28 | | f1of 5797 |
. . . . . . . . . . 11
    
      |
29 | 18, 28 | syl 17 |
. . . . . . . . . 10
       |
30 | 2, 3 | pmtrff1o 17115 |
. . . . . . . . . . . 12
       |
31 | 1, 30 | syl 17 |
. . . . . . . . . . 11
       |
32 | | f1of 5797 |
. . . . . . . . . . 11
    
      |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
       |
34 | | fco 5722 |
. . . . . . . . . 10
                   |
35 | 29, 33, 34 | syl2anc 671 |
. . . . . . . . 9
         |
36 | | fcoi1 5740 |
. . . . . . . . 9
                |
37 | 35, 36 | syl 17 |
. . . . . . . 8
          |
38 | 27, 37 | eqtrd 2486 |
. . . . . . 7
    
      |
39 | 24, 38 | syl5req 2499 |
. . . . . 6
           |
40 | 39 | ad2antrr 737 |
. . . . 5
      
         |
41 | | psgnunilem1.a |
. . . . . 6
    |
42 | 41 | ad2antrr 737 |
. . . . 5
         |
43 | 18 | adantr 471 |
. . . . . . . . . 10
 
 
   
         |
44 | 31 | adantr 471 |
. . . . . . . . . 10
 
 
   
         |
45 | 2, 3 | pmtrfb 17117 |
. . . . . . . . . . . . 13

         |
46 | 45 | simp3bi 1026 |
. . . . . . . . . . . 12
 
  |
47 | 12, 46 | syl 17 |
. . . . . . . . . . 11
 
  |
48 | 47 | adantr 471 |
. . . . . . . . . 10
 
 
   
      |
49 | | 2onn 7328 |
. . . . . . . . . . . . . . 15
 |
50 | | nnfi 7752 |
. . . . . . . . . . . . . . 15
   |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
 |
52 | 2, 3 | pmtrfb 17117 |
. . . . . . . . . . . . . . . . 17

         |
53 | 52 | simp3bi 1026 |
. . . . . . . . . . . . . . . 16
 
  |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . 15
 
  |
55 | | enfi 7775 |
. . . . . . . . . . . . . . 15
   
   |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . 14
      |
57 | 51, 56 | mpbiri 241 |
. . . . . . . . . . . . 13
 
  |
58 | 57 | adantr 471 |
. . . . . . . . . . . 12
 
 
   
   
  |
59 | 41 | adantr 471 |
. . . . . . . . . . . . . 14
 
 
   
  
   |
60 | | en2eleq 8426 |
. . . . . . . . . . . . . 14
     
           |
61 | 59, 48, 60 | syl2anc 671 |
. . . . . . . . . . . . 13
 
 
   
   
           |
62 | | simprl 769 |
. . . . . . . . . . . . . 14
 
 
   
  
   |
63 | | f1ofn 5798 |
. . . . . . . . . . . . . . . . . 18
    
  |
64 | 18, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
65 | 64 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
 
   
  
  |
66 | | imassrn 5157 |
. . . . . . . . . . . . . . . . . . 19
  
   |
67 | | frn 5718 |
. . . . . . . . . . . . . . . . . . 19
    
  |
68 | 66, 67 | syl5ss 3411 |
. . . . . . . . . . . . . . . . . 18
        

  |
69 | 29, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
    

  |
70 | 69 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
 
   
      

  |
71 | | simprr 771 |
. . . . . . . . . . . . . . . 16
 
 
   
  
       |
72 | | fnfvima 6129 |
. . . . . . . . . . . . . . . 16
          
                 |
73 | 65, 70, 71, 72 | syl3anc 1271 |
. . . . . . . . . . . . . . 15
 
 
   
                  |
74 | | difss 3528 |
. . . . . . . . . . . . . . . . . . . . 21
  |
75 | | dmss 5012 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
  |
77 | | f1odm 5801 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
78 | 18, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
79 | 76, 78 | syl5sseq 3448 |
. . . . . . . . . . . . . . . . . . 19
 
  |
80 | 79, 41 | sseldd 3401 |
. . . . . . . . . . . . . . . . . 18
   |
81 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . 19
   |
82 | 2, 3, 81 | pmtrffv 17111 |
. . . . . . . . . . . . . . . . . 18
 
                   |
83 | 12, 80, 82 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                   |
84 | 41 | iftrued 3857 |
. . . . . . . . . . . . . . . . 17
                     |
85 | 83, 84 | eqtrd 2486 |
. . . . . . . . . . . . . . . 16
             |
86 | 85 | adantr 471 |
. . . . . . . . . . . . . . 15
 
 
   
               |
87 | | imaco 5319 |
. . . . . . . . . . . . . . . . 17
    
            |
88 | 26 | imaeq1d 5145 |
. . . . . . . . . . . . . . . . . 18
      
 
       |
89 | | difss 3528 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
90 | | dmss 5012 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
  |
92 | | f1odm 5801 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
93 | 91, 92 | syl5sseq 3448 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
94 | 31, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
  |
95 | | resiima 5160 |
. . . . . . . . . . . . . . . . . . 19
     
     |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    
     |
97 | 88, 96 | eqtrd 2486 |
. . . . . . . . . . . . . . . . 17
      
    |
98 | 87, 97 | syl5eqr 2500 |
. . . . . . . . . . . . . . . 16
             |
99 | 98 | adantr 471 |
. . . . . . . . . . . . . . 15
 
 
   
               |
100 | 73, 86, 99 | 3eltr3d 2544 |
. . . . . . . . . . . . . 14
 
 
   
            |
101 | | prssi 4097 |
. . . . . . . . . . . . . 14
                   
   |
102 | 62, 100, 101 | syl2anc 671 |
. . . . . . . . . . . . 13
 
 
   
            
  |
103 | 61, 102 | eqsstrd 3434 |
. . . . . . . . . . . 12
 
 
   
       |
104 | 54 | ensymd 7607 |
. . . . . . . . . . . . . 14
    |
105 | | entr 7608 |
. . . . . . . . . . . . . 14
  
 
 
  |
106 | 47, 104, 105 | syl2anc 671 |
. . . . . . . . . . . . 13
 
   |
107 | 106 | adantr 471 |
. . . . . . . . . . . 12
 
 
   
       |
108 | | fisseneq 7770 |
. . . . . . . . . . . 12
  

   
 
  |
109 | 58, 103, 107, 108 | syl3anc 1271 |
. . . . . . . . . . 11
 
 
   
   
   |
110 | 109 | eqcomd 2458 |
. . . . . . . . . 10
 
 
   
   
   |
111 | | f1otrspeq 17099 |
. . . . . . . . . 10
                 
  |
112 | 43, 44, 48, 110, 111 | syl22anc 1272 |
. . . . . . . . 9
 
 
   
  
  |
113 | 112 | expr 624 |
. . . . . . . 8
 
  
        |
114 | 113 | necon3ad 2637 |
. . . . . . 7
 
  
        |
115 | 114 | imp 435 |
. . . . . 6
     
       |
116 | 16 | difeq1d 3518 |
. . . . . . . . . 10
     
     
  |
117 | 116 | dmeqd 5015 |
. . . . . . . . 9
     
        |
118 | | f1omvdconj 17098 |
. . . . . . . . . 10
                
       |
119 | 33, 18, 118 | syl2anc 671 |
. . . . . . . . 9
          
   |
120 | 117, 119 | eqtrd 2486 |
. . . . . . . 8
     
       |
121 | 120 | eleq2d 2515 |
. . . . . . 7
         
     |
122 | 121 | ad2antrr 737 |
. . . . . 6
      
    
        |
123 | 115, 122 | mtbird 307 |
. . . . 5
     
       |
124 | | coeq1 4970 |
. . . . . . . 8
               |
125 | 124 | eqeq2d 2462 |
. . . . . . 7
         
           |
126 | | difeq1 3512 |
. . . . . . . . . 10
     
       |
127 | 126 | dmeqd 5015 |
. . . . . . . . 9
     
       |
128 | 127 | eleq2d 2515 |
. . . . . . . 8
     

        |
129 | 128 | notbid 300 |
. . . . . . 7
     
         |
130 | 125, 129 | 3anbi13d 1345 |
. . . . . 6
             
 
       
         |
131 | | coeq2 4971 |
. . . . . . . 8
               |
132 | 131 | eqeq2d 2462 |
. . . . . . 7
         
           |
133 | | difeq1 3512 |
. . . . . . . . 9
 
   |
134 | 133 | dmeqd 5015 |
. . . . . . . 8
 
   |
135 | 134 | eleq2d 2515 |
. . . . . . 7
 

    |
136 | 132, 135 | 3anbi12d 1344 |
. . . . . 6
                 
 
       
         |
137 | 130, 136 | rspc2ev 3129 |
. . . . 5
     
         
       

          |
138 | 22, 23, 40, 42, 123, 137 | syl113anc 1283 |
. . . 4
      

 
   
    |
139 | 138 | olcd 399 |
. . 3
          

    

     |
140 | 11, 139 | pm2.61dane 2711 |
. 2
 
      

    

     |
141 | 1 | adantr 471 |
. . . 4
 
    |
142 | | coass 5333 |
. . . . . . 7
     
   |
143 | 2, 3 | pmtrfcnv 17116 |
. . . . . . . . . 10
 
  |
144 | 1, 143 | syl 17 |
. . . . . . . . 9
 
  |
145 | 144 | eqcomd 2458 |
. . . . . . . 8
    |
146 | 145 | coeq2d 4975 |
. . . . . . 7
            |
147 | 142, 146 | syl5eqr 2500 |
. . . . . 6
  
         |
148 | 2, 3 | pmtrfconj 17118 |
. . . . . . 7
              |
149 | 12, 31, 148 | syl2anc 671 |
. . . . . 6
        |
150 | 147, 149 | eqeltrd 2530 |
. . . . 5
  
    |
151 | 150 | adantr 471 |
. . . 4
 
  
     |
152 | 5 | coeq1d 4974 |
. . . . . . 7
    
  
      |
153 | | fcoi2 5741 |
. . . . . . . 8
                |
154 | 35, 153 | syl 17 |
. . . . . . 7
          |
155 | 152, 154 | eqtr2d 2487 |
. . . . . 6
           |
156 | | coass 5333 |
. . . . . 6
       
     |
157 | 155, 156 | syl6eq 2502 |
. . . . 5
     
     |
158 | 157 | adantr 471 |
. . . 4
 
  
  

     |
159 | | f1ofn 5798 |
. . . . . . . . . 10
    
  |
160 | 31, 159 | syl 17 |
. . . . . . . . 9
   |
161 | | fnelnfp 6079 |
. . . . . . . . 9
 
  
       |
162 | 160, 80, 161 | syl2anc 671 |
. . . . . . . 8
  
       |
163 | 162 | necon2bbid 2667 |
. . . . . . 7
     

   |
164 | 163 | biimpar 492 |
. . . . . 6
 
        |
165 | | fnfvima 6129 |
. . . . . . . 8
            
   |
166 | 160, 79, 41, 165 | syl3anc 1271 |
. . . . . . 7
       
    |
167 | 166 | adantr 471 |
. . . . . 6
 
         
   |
168 | 164, 167 | eqeltrrd 2531 |
. . . . 5
 
     
   |
169 | 147 | difeq1d 3518 |
. . . . . . . 8
   
 
     
  |
170 | 169 | dmeqd 5015 |
. . . . . . 7
     
        |
171 | | f1omvdconj 17098 |
. . . . . . . 8
                
       |
172 | 29, 31, 171 | syl2anc 671 |
. . . . . . 7
          
   |
173 | 170, 172 | eqtrd 2486 |
. . . . . 6
     
       |
174 | 173 | adantr 471 |
. . . . 5
 
    
 
       |
175 | 168, 174 | eleqtrrd 2533 |
. . . 4
 
         |
176 | | simpr 467 |
. . . 4
 
 
   |
177 | | coeq1 4970 |
. . . . . . 7
       |
178 | 177 | eqeq2d 2462 |
. . . . . 6
     
       |
179 | | difeq1 3512 |
. . . . . . . . 9
 
   |
180 | 179 | dmeqd 5015 |
. . . . . . . 8
 
   |
181 | 180 | eleq2d 2515 |
. . . . . . 7
 

    |
182 | 181 | notbid 300 |
. . . . . 6
 
 
   |
183 | 178, 182 | 3anbi13d 1345 |
. . . . 5
         
 
   
     |
184 | | coeq2 4971 |
. . . . . . 7
  
  
  

     |
185 | 184 | eqeq2d 2462 |
. . . . . 6
  
      
           |
186 | | difeq1 3512 |
. . . . . . . 8
  
  
       |
187 | 186 | dmeqd 5015 |
. . . . . . 7
  
  
       |
188 | 187 | eleq2d 2515 |
. . . . . 6
  
  

  
     |
189 | 185, 188 | 3anbi12d 1344 |
. . . . 5
  
          
 
  

       
     |
190 | 183, 189 | rspc2ev 3129 |
. . . 4
  

             
     

          |
191 | 141, 151,
158, 175, 176, 190 | syl113anc 1283 |
. . 3
 
  

 
   
    |
192 | 191 | olcd 399 |
. 2
 
      

    

     |
193 | 140, 192 | pm2.61dan 805 |
1
   
  
           |