Proof of Theorem ramub1lem1
Step | Hyp | Ref
| Expression |
1 | | ramub1.v |
. . . . . . . 8

  |
2 | | ramub1.w |
. . . . . . . 8

      |
3 | 1, 2 | sstrd 3441 |
. . . . . . 7

      |
4 | 3 | difss2d 3562 |
. . . . . 6

  |
5 | | ramub1.x |
. . . . . . 7
   |
6 | 5 | snssd 4116 |
. . . . . 6
     |
7 | 4, 6 | unssd 3609 |
. . . . 5
       |
8 | | ramub1.4 |
. . . . . 6
   |
9 | | elpw2g 4565 |
. . . . . 6
              |
10 | 8, 9 | syl 17 |
. . . . 5
      
       |
11 | 7, 10 | mpbird 236 |
. . . 4
        |
12 | 11 | adantr 467 |
. . 3
 
 
      |
13 | | iftrue 3886 |
. . . . . . 7
  
                     |
14 | 13 | adantl 468 |
. . . . . 6
 
  
                     |
15 | | ramub1.9 |
. . . . . . 7
                      |
16 | 15 | adantr 467 |
. . . . . 6
 
  
            
      |
17 | 14, 16 | eqbrtrrd 4424 |
. . . . 5
 
             |
18 | | ramub1.f |
. . . . . . . . 9
       |
19 | | ramub1.d |
. . . . . . . . 9
   |
20 | 18, 19 | ffvelrnd 6021 |
. . . . . . . 8
       |
21 | 20 | adantr 467 |
. . . . . . 7
 
       |
22 | 21 | nnred 10621 |
. . . . . 6
 
       |
23 | | 1red 9655 |
. . . . . 6
 
   |
24 | | ssfi 7789 |
. . . . . . . . 9
  
  |
25 | 8, 4, 24 | syl2anc 666 |
. . . . . . . 8
   |
26 | | hashcl 12535 |
. . . . . . . 8
       |
27 | | nn0re 10875 |
. . . . . . . 8
    
      |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . 7
       |
29 | 28 | adantr 467 |
. . . . . 6
 
       |
30 | 22, 23, 29 | lesubaddd 10207 |
. . . . 5
 
       
                 |
31 | 17, 30 | mpbid 214 |
. . . 4
 
             |
32 | | fveq2 5863 |
. . . . 5
           |
33 | | snidg 3993 |
. . . . . . . 8
     |
34 | 5, 33 | syl 17 |
. . . . . . 7
     |
35 | 3 | sseld 3430 |
. . . . . . . 8
         |
36 | | eldifn 3555 |
. . . . . . . 8
    
    |
37 | 35, 36 | syl6 34 |
. . . . . . 7
       |
38 | 34, 37 | mt2d 121 |
. . . . . 6
   |
39 | | hashunsng 12568 |
. . . . . . 7
   
   
             |
40 | 5, 39 | syl 17 |
. . . . . 6
  
                  |
41 | 25, 38, 40 | mp2and 684 |
. . . . 5
    
            |
42 | 32, 41 | breqan12rd 4418 |
. . . 4
 
     
   
   
             |
43 | 31, 42 | mpbird 236 |
. . 3
 
        
      |
44 | | snfi 7647 |
. . . . . . 7
 
 |
45 | | unfi 7835 |
. . . . . . 7
           |
46 | 25, 44, 45 | sylancl 667 |
. . . . . 6
       |
47 | | ramub1.m |
. . . . . . 7
   |
48 | 47 | nnnn0d 10922 |
. . . . . 6
   |
49 | | ramub1.3 |
. . . . . . 7
 
 
       |
50 | 49 | hashbcval 14947 |
. . . . . 6
                 
          |
51 | 46, 48, 50 | syl2anc 666 |
. . . . 5
           
          |
52 | 51 | adantr 467 |
. . . 4
 
                      |
53 | | simpl1l 1058 |
. . . . . . . 8
   

 
            |
54 | 49 | hashbcval 14947 |
. . . . . . . . . 10
 
              |
55 | 25, 48, 54 | syl2anc 666 |
. . . . . . . . 9
              |
56 | | ramub1.s |
. . . . . . . . 9
    
         |
57 | 55, 56 | eqsstr3d 3466 |
. . . . . . . 8
  
              |
58 | 53, 57 | syl 17 |
. . . . . . 7
   

 
          

              |
59 | | simpr 463 |
. . . . . . . 8
   

 
         
   |
60 | | simpl3 1012 |
. . . . . . . 8
   

 
                |
61 | | rabid 2966 |
. . . . . . . 8
       
         |
62 | 59, 60, 61 | sylanbrc 669 |
. . . . . . 7
   

 
         
         |
63 | 58, 62 | sseldd 3432 |
. . . . . 6
   

 
         
         |
64 | | simpl2 1011 |
. . . . . . . . . . . 12
   

 
       
 
       |
65 | 64 | elpwid 3960 |
. . . . . . . . . . 11
   

 
       
 

     |
66 | | simpl1l 1058 |
. . . . . . . . . . . 12
   

 
       
 
  |
67 | 66, 7 | syl 17 |
. . . . . . . . . . 11
   

 
       
 
      |
68 | 65, 67 | sstrd 3441 |
. . . . . . . . . 10
   

 
       
 
  |
69 | | vex 3047 |
. . . . . . . . . . 11
 |
70 | 69 | elpw 3956 |
. . . . . . . . . 10
 
  |
71 | 68, 70 | sylibr 216 |
. . . . . . . . 9
   

 
       
 
   |
72 | | simpl3 1012 |
. . . . . . . . 9
   

 
       
 
      |
73 | | rabid 2966 |
. . . . . . . . 9
       
         |
74 | 71, 72, 73 | sylanbrc 669 |
. . . . . . . 8
   

 
       
 
         |
75 | 49 | hashbcval 14947 |
. . . . . . . . . 10
 
              |
76 | 8, 48, 75 | syl2anc 666 |
. . . . . . . . 9
              |
77 | 66, 76 | syl 17 |
. . . . . . . 8
   

 
       
 
             |
78 | 74, 77 | eleqtrrd 2531 |
. . . . . . 7
   

 
       
 
      |
79 | 2 | difss2d 3562 |
. . . . . . . . . . . . . . 15

  |
80 | | ssfi 7789 |
. . . . . . . . . . . . . . 15
  
  |
81 | 8, 79, 80 | syl2anc 666 |
. . . . . . . . . . . . . 14
   |
82 | | nnm1nn0 10908 |
. . . . . . . . . . . . . . 15
 
   |
83 | 47, 82 | syl 17 |
. . . . . . . . . . . . . 14
     |
84 | 49 | hashbcval 14947 |
. . . . . . . . . . . . . 14
  
                   |
85 | 81, 83, 84 | syl2anc 666 |
. . . . . . . . . . . . 13
                  |
86 | | ramub1.8 |
. . . . . . . . . . . . 13
      
         |
87 | 85, 86 | eqsstr3d 3466 |
. . . . . . . . . . . 12
  
                |
88 | 66, 87 | syl 17 |
. . . . . . . . . . 11
   

 
       
 
                  |
89 | | uncom 3577 |
. . . . . . . . . . . . . . . 16
         |
90 | 65, 89 | syl6sseq 3477 |
. . . . . . . . . . . . . . 15
   

 
       
 
      |
91 | | ssundif 3850 |
. . . . . . . . . . . . . . 15
   
       |
92 | 90, 91 | sylib 200 |
. . . . . . . . . . . . . 14
   

 
       
 
      |
93 | 66, 1 | syl 17 |
. . . . . . . . . . . . . 14
   

 
       
 
  |
94 | 92, 93 | sstrd 3441 |
. . . . . . . . . . . . 13
   

 
       
 
      |
95 | | difexg 4550 |
. . . . . . . . . . . . . . 15
 
     |
96 | 69, 95 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
97 | 96 | elpw 3956 |
. . . . . . . . . . . . 13
            |
98 | 94, 97 | sylibr 216 |
. . . . . . . . . . . 12
   

 
       
 
       |
99 | 66, 8 | syl 17 |
. . . . . . . . . . . . . . . . 17
   

 
       
 
  |
100 | | ssfi 7789 |
. . . . . . . . . . . . . . . . 17
  
  |
101 | 99, 68, 100 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
   

 
       
 
  |
102 | | diffi 7800 |
. . . . . . . . . . . . . . . 16
 
     |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . 15
   

 
       
 
      |
104 | | hashcl 12535 |
. . . . . . . . . . . . . . 15
        
      |
105 | | nn0cn 10876 |
. . . . . . . . . . . . . . 15
                   |
106 | 103, 104,
105 | 3syl 18 |
. . . . . . . . . . . . . 14
   

 
       
 
   
      |
107 | | ax-1cn 9594 |
. . . . . . . . . . . . . 14
 |
108 | | pncan 9878 |
. . . . . . . . . . . . . 14
     
          
                |
109 | 106, 107,
108 | sylancl 667 |
. . . . . . . . . . . . 13
   

 
       
 
               
      |
110 | | neldifsnd 4099 |
. . . . . . . . . . . . . . . 16
   

 
       
 
      |
111 | | hashunsng 12568 |
. . . . . . . . . . . . . . . . 17
      
                     
        |
112 | 66, 5, 111 | 3syl 18 |
. . . . . . . . . . . . . . . 16
   

 
       
 
                           
        |
113 | 103, 110,
112 | mp2and 684 |
. . . . . . . . . . . . . . 15
   

 
       
 
                
       |
114 | | undif1 3841 |
. . . . . . . . . . . . . . . . . 18
             |
115 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
   

 
       
 
   |
116 | 64, 115 | eldifd 3414 |
. . . . . . . . . . . . . . . . . . . . 21
   

 
       
 
          |
117 | | elpwunsn 4011 |
. . . . . . . . . . . . . . . . . . . . 21
   
       |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   

 
       
 
  |
119 | 118 | snssd 4116 |
. . . . . . . . . . . . . . . . . . 19
   

 
       
 
    |
120 | | ssequn2 3606 |
. . . . . . . . . . . . . . . . . . 19
         |
121 | 119, 120 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
   

 
       
 
      |
122 | 114, 121 | syl5req 2497 |
. . . . . . . . . . . . . . . . 17
   

 
       
 
          |
123 | 122 | fveq2d 5867 |
. . . . . . . . . . . . . . . 16
   

 
       
 
                  |
124 | 123, 72 | eqtr3d 2486 |
. . . . . . . . . . . . . . 15
   

 
       
 
              |
125 | 113, 124 | eqtr3d 2486 |
. . . . . . . . . . . . . 14
   

 
       
 
            |
126 | 125 | oveq1d 6303 |
. . . . . . . . . . . . 13
   

 
       
 
                |
127 | 109, 126 | eqtr3d 2486 |
. . . . . . . . . . . 12
   

 
       
 
   
        |
128 | | fveq2 5863 |
. . . . . . . . . . . . . 14
            
      |
129 | 128 | eqeq1d 2452 |
. . . . . . . . . . . . 13
           
   
         |
130 | 129 | elrab 3195 |
. . . . . . . . . . . 12
                                 |
131 | 98, 127, 130 | sylanbrc 669 |
. . . . . . . . . . 11
   

 
       
 
               |
132 | 88, 131 | sseldd 3432 |
. . . . . . . . . 10
   

 
       
 
             |
133 | | ramub1.h |
. . . . . . . . . . . 12
              
      |
134 | 133 | mptiniseg 5328 |
. . . . . . . . . . 11
                              |
135 | 66, 19, 134 | 3syl 18 |
. . . . . . . . . 10
   

 
       
 
                             |
136 | 132, 135 | eleqtrd 2530 |
. . . . . . . . 9
   

 
       
 
                          |
137 | | uneq1 3580 |
. . . . . . . . . . . . 13
                   |
138 | 137 | fveq2d 5867 |
. . . . . . . . . . . 12
                           |
139 | 138 | eqeq1d 2452 |
. . . . . . . . . . 11
         
                   |
140 | 139 | elrab 3195 |
. . . . . . . . . 10
                                                       |
141 | 140 | simprbi 466 |
. . . . . . . . 9
                                       |
142 | 136, 141 | syl 17 |
. . . . . . . 8
   

 
       
 
              |
143 | 122 | fveq2d 5867 |
. . . . . . . 8
   

 
       
 
                  |
144 | | simpl1r 1059 |
. . . . . . . 8
   

 
       
 
  |
145 | 142, 143,
144 | 3eqtr4d 2494 |
. . . . . . 7
   

 
       
 
      |
146 | | ramub1.6 |
. . . . . . . . 9
           |
147 | | ffn 5726 |
. . . . . . . . 9
        
      |
148 | 146, 147 | syl 17 |
. . . . . . . 8
       |
149 | | fniniseg 6001 |
. . . . . . . 8
            
             |
150 | 66, 148, 149 | 3syl 18 |
. . . . . . 7
   

 
       
 
       
             |
151 | 78, 145, 150 | mpbir2and 932 |
. . . . . 6
   

 
       
 
         |
152 | 63, 151 | pm2.61dan 799 |
. . . . 5
             
         |
153 | 152 | rabssdv 3508 |
. . . 4
 
                     |
154 | 52, 153 | eqsstrd 3465 |
. . 3
 
        
         |
155 | | fveq2 5863 |
. . . . . 6
            
      |
156 | 155 | breq2d 4413 |
. . . . 5
             
               |
157 | | oveq1 6295 |
. . . . . 6
                   |
158 | 157 | sseq1d 3458 |
. . . . 5
                
 
     
          |
159 | 156, 158 | anbi12d 716 |
. . . 4
                          
        
                       |
160 | 159 | rspcev 3149 |
. . 3
                           
         
                        |
161 | 12, 43, 154, 160 | syl12anc 1265 |
. 2
 
           
              |
162 | | elpw2g 4565 |
. . . . . 6
 
    |
163 | 8, 162 | syl 17 |
. . . . 5
  
   |
164 | 4, 163 | mpbird 236 |
. . . 4
    |
165 | 164 | adantr 467 |
. . 3
 

   |
166 | | ifnefalse 3892 |
. . . . 5
  
                   |
167 | 166 | adantl 468 |
. . . 4
 

 
                   |
168 | 15 | adantr 467 |
. . . 4
 

 
                   |
169 | 167, 168 | eqbrtrrd 4424 |
. . 3
 

          |
170 | 56 | adantr 467 |
. . 3
 

             |
171 | | fveq2 5863 |
. . . . . 6
           |
172 | 171 | breq2d 4413 |
. . . . 5
     
               |
173 | | oveq1 6295 |
. . . . . 6
           |
174 | 173 | sseq1d 3458 |
. . . . 5
     
                     |
175 | 172, 174 | anbi12d 716 |
. . . 4
              
       
        
               |
176 | 175 | rspcev 3149 |
. . 3
                                   
              |
177 | 165, 169,
170, 176 | syl12anc 1265 |
. 2
 

          
              |
178 | 161, 177 | pm2.61dane 2710 |
1
                          |