Step | Hyp | Ref
| Expression |
1 | | lbsext.k |
. . . 4
    |
2 | | lbsext.s |
. . . . 5
 
 
   
       |
3 | | ssrab2 3548 |
. . . . 5
                |
4 | 2, 3 | eqsstri 3497 |
. . . 4
  |
5 | | ssnum 8323 |
. . . 4
  
 
  |
6 | 1, 4, 5 | sylancl 662 |
. . 3
   |
7 | | lbsext.v |
. . . 4
     |
8 | | lbsext.j |
. . . 4
LBasis   |
9 | | lbsext.n |
. . . 4
     |
10 | | lbsext.w |
. . . 4
   |
11 | | lbsext.c |
. . . 4

  |
12 | | lbsext.x |
. . . 4
 
          |
13 | 7, 8, 9, 10, 11, 12, 2 | lbsextlem1 17365 |
. . 3
   |
14 | 10 | adantr 465 |
. . . . . 6
 
 [ ]
    |
15 | 11 | adantr 465 |
. . . . . 6
 
 [ ]
    |
16 | 12 | adantr 465 |
. . . . . 6
 
 [ ]
  
          |
17 | | eqid 2454 |
. . . . . 6
         |
18 | | simpr1 994 |
. . . . . 6
 
 [ ]
    |
19 | | simpr2 995 |
. . . . . 6
 
 [ ]
    |
20 | | simpr3 996 |
. . . . . 6
 
 [ ]
  [ ]   |
21 | | eqid 2454 |
. . . . . 6

            
     |
22 | 7, 8, 9, 14, 15, 16, 2, 17, 18, 19, 20, 21 | lbsextlem3 17367 |
. . . . 5
 
 [ ]
     |
23 | 22 | ex 434 |
. . . 4
   [ ]      |
24 | 23 | alrimiv 1686 |
. . 3
    
[ ] 
    |
25 | | zornn0g 8788 |
. . 3
     
[ ] 
   

  |
26 | 6, 13, 24, 25 | syl3anc 1219 |
. 2
  
  |
27 | | simprl 755 |
. . . . . . . . 9
 


    |
28 | | sseq2 3489 |
. . . . . . . . . . 11
 
   |
29 | | difeq1 3578 |
. . . . . . . . . . . . . . 15
 
         |
30 | 29 | fveq2d 5806 |
. . . . . . . . . . . . . 14
                   |
31 | 30 | eleq2d 2524 |
. . . . . . . . . . . . 13
         
           |
32 | 31 | notbid 294 |
. . . . . . . . . . . 12
 
       
           |
33 | 32 | raleqbi1dv 3031 |
. . . . . . . . . . 11
  
                    |
34 | 28, 33 | anbi12d 710 |
. . . . . . . . . 10
            
 
   
        |
35 | 34, 2 | elrab2 3226 |
. . . . . . . . 9

   
            |
36 | 27, 35 | sylib 196 |
. . . . . . . 8
 


         
        |
37 | 36 | simpld 459 |
. . . . . . 7
 


     |
38 | 37 | elpwid 3981 |
. . . . . 6
 


 
  |
39 | | lveclmod 17313 |
. . . . . . . . . 10

  |
40 | 10, 39 | syl 16 |
. . . . . . . . 9
   |
41 | 40 | adantr 465 |
. . . . . . . 8
 


 
  |
42 | 7, 9 | lspssv 17190 |
. . . . . . . 8
         |
43 | 41, 38, 42 | syl2anc 661 |
. . . . . . 7
 


     
  |
44 | | ssun1 3630 |
. . . . . . . . . . . 12
     |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
             
      |
46 | | ssun2 3631 |
. . . . . . . . . . . . . 14
       |
47 | | ssnid 4017 |
. . . . . . . . . . . . . 14
   |
48 | 46, 47 | sselii 3464 |
. . . . . . . . . . . . 13
     |
49 | 7, 9 | lspssid 17192 |
. . . . . . . . . . . . . . . 16
         |
50 | 41, 38, 49 | syl2anc 661 |
. . . . . . . . . . . . . . 15
 


 
      |
51 | 50 | adantr 465 |
. . . . . . . . . . . . . 14
             
      |
52 | | eldifn 3590 |
. . . . . . . . . . . . . . 15
      
      |
53 | 52 | adantl 466 |
. . . . . . . . . . . . . 14
             
      |
54 | 51, 53 | ssneldd 3470 |
. . . . . . . . . . . . 13
             
  |
55 | | nelne1 2781 |
. . . . . . . . . . . . 13
     
       |
56 | 48, 54, 55 | sylancr 663 |
. . . . . . . . . . . 12
             
      |
57 | 56 | necomd 2723 |
. . . . . . . . . . 11
             
      |
58 | | df-pss 3455 |
. . . . . . . . . . 11
                 |
59 | 45, 57, 58 | sylanbrc 664 |
. . . . . . . . . 10
             
      |
60 | 38 | adantr 465 |
. . . . . . . . . . . . . 14
             
  |
61 | | eldifi 3589 |
. . . . . . . . . . . . . . . 16
         |
62 | 61 | adantl 466 |
. . . . . . . . . . . . . . 15
             
  |
63 | 62 | snssd 4129 |
. . . . . . . . . . . . . 14
             
    |
64 | 60, 63 | unssd 3643 |
. . . . . . . . . . . . 13
             
      |
65 | | fvex 5812 |
. . . . . . . . . . . . . . 15
     |
66 | 7, 65 | eqeltri 2538 |
. . . . . . . . . . . . . 14
 |
67 | 66 | elpw2 4567 |
. . . . . . . . . . . . 13
            |
68 | 64, 67 | sylibr 212 |
. . . . . . . . . . . 12
             
       |
69 | 36 | simprd 463 |
. . . . . . . . . . . . . . . 16
 


               |
70 | 69 | simpld 459 |
. . . . . . . . . . . . . . 15
 


    |
71 | 70 | adantr 465 |
. . . . . . . . . . . . . 14
             
  |
72 | 71, 44 | syl6ss 3479 |
. . . . . . . . . . . . 13
             
      |
73 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
             

                 |
74 | 38 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
             

                 |
75 | 74 | ssdifssd 3605 |
. . . . . . . . . . . . . . . . . . . 20
             

                     |
76 | 62 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
             

                 |
77 | | simprrr 764 |
. . . . . . . . . . . . . . . . . . . . . 22
             

                             |
78 | | simprrl 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             

                 |
79 | 54 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             

              
  |
80 | | nelne2 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

  |
81 | 78, 79, 80 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             

                 |
82 | | elsni 4013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
83 | 82 | necon3ai 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    |
84 | 81, 83 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             

              
    |
85 | | disjsn 4047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
86 | 84, 85 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             

                       |
87 | | disj3 3834 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
88 | 86, 87 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             

                         |
89 | 88 | uneq2d 3621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             

                                     |
90 | | difundir 3714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
91 | 89, 90 | syl6reqr 2514 |
. . . . . . . . . . . . . . . . . . . . . . 23
             

                   
             |
92 | 91 | fveq2d 5806 |
. . . . . . . . . . . . . . . . . . . . . 22
             

                                         |
93 | 77, 92 | eleqtrd 2544 |
. . . . . . . . . . . . . . . . . . . . 21
             

                             |
94 | 69 | simprd 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
 


  
          |
95 | 94 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . 22
             

                          |
96 | | rsp 2894 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        
   
       |
97 | 95, 78, 96 | sylc 60 |
. . . . . . . . . . . . . . . . . . . . 21
             

              
          |
98 | 93, 97 | eldifd 3450 |
. . . . . . . . . . . . . . . . . . . 20
             

                                       |
99 | 7, 17, 9 | lspsolv 17350 |
. . . . . . . . . . . . . . . . . . . 20
      
                                      |
100 | 73, 75, 76, 98, 99 | syl13anc 1221 |
. . . . . . . . . . . . . . . . . . 19
             

                             |
101 | | undif1 3865 |
. . . . . . . . . . . . . . . . . . . . 21
             |
102 | 78 | snssd 4129 |
. . . . . . . . . . . . . . . . . . . . . 22
             

                   |
103 | | ssequn2 3640 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
104 | 102, 103 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . 21
             

                     |
105 | 101, 104 | syl5eq 2507 |
. . . . . . . . . . . . . . . . . . . 20
             

                         |
106 | 105 | fveq2d 5806 |
. . . . . . . . . . . . . . . . . . 19
             

                                 |
107 | 100, 106 | eleqtrd 2544 |
. . . . . . . . . . . . . . . . . 18
             

                     |
108 | 107 | expr 615 |
. . . . . . . . . . . . . . . . 17
             
 
            
       |
109 | 53, 108 | mtod 177 |
. . . . . . . . . . . . . . . 16
             

               |
110 | | imnan 422 |
. . . . . . . . . . . . . . . 16
 
            

               |
111 | 109, 110 | sylibr 212 |
. . . . . . . . . . . . . . 15
             

               |
112 | 111 | ralrimiv 2828 |
. . . . . . . . . . . . . 14
             

              |
113 | | difssd 3595 |
. . . . . . . . . . . . . . . . . 18
 


        |
114 | 7, 9 | lspss 17191 |
. . . . . . . . . . . . . . . . . 18
     
    
          |
115 | 41, 38, 113, 114 | syl3anc 1219 |
. . . . . . . . . . . . . . . . 17
 


     
          |
116 | 115 | adantr 465 |
. . . . . . . . . . . . . . . 16
             
              |
117 | 116, 53 | ssneldd 3470 |
. . . . . . . . . . . . . . 15
             
   
      |
118 | | vex 3081 |
. . . . . . . . . . . . . . . 16
 |
119 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
120 | | sneq 3998 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
121 | 120 | difeq2d 3585 |
. . . . . . . . . . . . . . . . . . . 20
             
     |
122 | | difun2 3869 |
. . . . . . . . . . . . . . . . . . . 20
             |
123 | 121, 122 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . 19
               |
124 | 123 | fveq2d 5806 |
. . . . . . . . . . . . . . . . . 18
                       |
125 | 119, 124 | eleq12d 2536 |
. . . . . . . . . . . . . . . . 17
         
   
           |
126 | 125 | notbid 294 |
. . . . . . . . . . . . . . . 16
 
           
           |
127 | 118, 126 | ralsn 4026 |
. . . . . . . . . . . . . . 15
 
             
          |
128 | 117, 127 | sylibr 212 |
. . . . . . . . . . . . . 14
             
  
              |
129 | | ralun 3649 |
. . . . . . . . . . . . . 14
                 
             
                  |
130 | 112, 128,
129 | syl2anc 661 |
. . . . . . . . . . . . 13
             
            
      |
131 | 72, 130 | jca 532 |
. . . . . . . . . . . 12
             
                         |
132 | | sseq2 3489 |
. . . . . . . . . . . . . 14
     
       |
133 | | difeq1 3578 |
. . . . . . . . . . . . . . . . . 18
             
     |
134 | 133 | fveq2d 5806 |
. . . . . . . . . . . . . . . . 17
                           |
135 | 134 | eleq2d 2524 |
. . . . . . . . . . . . . . . 16
         
   
               |
136 | 135 | notbid 294 |
. . . . . . . . . . . . . . 15
         
   
               |
137 | 136 | raleqbi1dv 3031 |
. . . . . . . . . . . . . 14
      
   
   
            
       |
138 | 132, 137 | anbi12d 710 |
. . . . . . . . . . . . 13
       
                                   |
139 | 138, 2 | elrab2 3226 |
. . . . . . . . . . . 12
                            
        |
140 | 68, 131, 139 | sylanbrc 664 |
. . . . . . . . . . 11
             
      |
141 | | simplrr 760 |
. . . . . . . . . . 11
             

  |
142 | | psseq2 3555 |
. . . . . . . . . . . . 13
     
       |
143 | 142 | notbid 294 |
. . . . . . . . . . . 12
     
       |
144 | 143 | rspcv 3175 |
. . . . . . . . . . 11
      
       |
145 | 140, 141,
144 | sylc 60 |
. . . . . . . . . 10
             
      |
146 | 59, 145 | pm2.65da 576 |
. . . . . . . . 9
 


 
        |
147 | 146 | eq0rdv 3783 |
. . . . . . . 8
 


          |
148 | | ssdif0 3848 |
. . . . . . . 8
    
        |
149 | 147, 148 | sylibr 212 |
. . . . . . 7
 


        |
150 | 43, 149 | eqssd 3484 |
. . . . . 6
 


        |
151 | 10 | adantr 465 |
. . . . . . 7
 


 
  |
152 | 7, 8, 9 | islbs2 17361 |
. . . . . . 7


     
   
        |
153 | 151, 152 | syl 16 |
. . . . . 6
 


   
    
            |
154 | 38, 150, 94, 153 | mpbir3and 1171 |
. . . . 5
 


    |
155 | 154, 70 | jca 532 |
. . . 4
 


  
   |
156 | 155 | ex 434 |
. . 3
   
      |
157 | 156 | reximdv2 2931 |
. 2
        |
158 | 26, 157 | mpd 15 |
1
    |