Step | Hyp | Ref
| Expression |
1 | | lbsext.a |
. . . . 5

  |
2 | | lbsext.s |
. . . . . 6
 
 
   
       |
3 | | ssrab2 3513 |
. . . . . 6
                |
4 | 2, 3 | eqsstri 3461 |
. . . . 5
  |
5 | 1, 4 | syl6ss 3443 |
. . . 4

   |
6 | | sspwuni 4366 |
. . . 4
 
   |
7 | 5, 6 | sylib 200 |
. . 3
    |
8 | | lbsext.v |
. . . . 5
     |
9 | | fvex 5873 |
. . . . 5
     |
10 | 8, 9 | eqeltri 2524 |
. . . 4
 |
11 | 10 | elpw2 4566 |
. . 3
 
 
  |
12 | 7, 11 | sylibr 216 |
. 2
     |
13 | | ssintub 4251 |
. . . . 5
  
  |
14 | | simpl 459 |
. . . . . . . . . 10
 
            |
15 | 14 | a1i 11 |
. . . . . . . . 9
        
        |
16 | 15 | ss2rabi 3510 |
. . . . . . . 8
                  |
17 | 2, 16 | eqsstri 3461 |
. . . . . . 7
 
  |
18 | 1, 17 | syl6ss 3443 |
. . . . . 6

     |
19 | | intss 4254 |
. . . . . 6
           |
20 | 18, 19 | syl 17 |
. . . . 5
        |
21 | 13, 20 | syl5ss 3442 |
. . . 4

   |
22 | | lbsext.z |
. . . . 5
   |
23 | | intssuni 4256 |
. . . . 5

    |
24 | 22, 23 | syl 17 |
. . . 4
     |
25 | 21, 24 | sstrd 3441 |
. . 3

   |
26 | | eluni2 4201 |
. . . . 5
 

  |
27 | | simpll1 1046 |
. . . . . . . . . . . 12
   


           |
28 | | lbsext.w |
. . . . . . . . . . . . 13
   |
29 | | lveclmod 18322 |
. . . . . . . . . . . . 13

  |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
   |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
   


        
  |
32 | 27, 1 | syl 17 |
. . . . . . . . . . . . . . 15
   


           |
33 | | lbsext.r |
. . . . . . . . . . . . . . . . 17
 [ ]
  |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
   


         [ ]   |
35 | | simpll2 1047 |
. . . . . . . . . . . . . . . 16
   


           |
36 | | simplr 761 |
. . . . . . . . . . . . . . . 16
   


        
  |
37 | | sorpssun 6575 |
. . . . . . . . . . . . . . . 16
 [ ] 
 
    |
38 | 34, 35, 36, 37 | syl12anc 1265 |
. . . . . . . . . . . . . . 15
   


             |
39 | 32, 38 | sseldd 3432 |
. . . . . . . . . . . . . 14
   


             |
40 | 4, 39 | sseldi 3429 |
. . . . . . . . . . . . 13
   


              |
41 | 40 | elpwid 3960 |
. . . . . . . . . . . 12
   


          
  |
42 | 41 | ssdifssd 3570 |
. . . . . . . . . . 11
   


                 |
43 | | ssun2 3597 |
. . . . . . . . . . . 12
   |
44 | | ssdif 3567 |
. . . . . . . . . . . 12
   
     
     |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . 11
   


                     |
46 | | lbsext.n |
. . . . . . . . . . . 12
     |
47 | 8, 46 | lspss 18200 |
. . . . . . . . . . 11
    
                 
                |
48 | 31, 42, 45, 47 | syl3anc 1267 |
. . . . . . . . . 10
   


            
                |
49 | | simpr 463 |
. . . . . . . . . 10
   


        
          |
50 | 48, 49 | sseldd 3432 |
. . . . . . . . 9
   


        
            |
51 | | sseq2 3453 |
. . . . . . . . . . . . . . 15
   
     |
52 | | difeq1 3543 |
. . . . . . . . . . . . . . . . . . 19
   
     
     |
53 | 52 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
                       |
54 | 53 | eleq2d 2513 |
. . . . . . . . . . . . . . . . 17
           
             |
55 | 54 | notbid 296 |
. . . . . . . . . . . . . . . 16
   
       
             |
56 | 55 | raleqbi1dv 2994 |
. . . . . . . . . . . . . . 15
    
                        |
57 | 51, 56 | anbi12d 716 |
. . . . . . . . . . . . . 14
              
  
        
        |
58 | 57, 2 | elrab2 3197 |
. . . . . . . . . . . . 13
  
    
                   |
59 | 58 | simprbi 466 |
. . . . . . . . . . . 12
      
       
       |
60 | 59 | simprd 465 |
. . . . . . . . . . 11
           
      |
61 | 39, 60 | syl 17 |
. . . . . . . . . 10
   


         
              |
62 | | simpll3 1048 |
. . . . . . . . . . 11
   


        
  |
63 | | elun1 3600 |
. . . . . . . . . . 11
     |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
   


        
    |
65 | | rsp 2753 |
. . . . . . . . . 10
 
       
      
             |
66 | 61, 64, 65 | sylc 62 |
. . . . . . . . 9
   


        
            |
67 | 50, 66 | pm2.65da 579 |
. . . . . . . 8
  
 
          |
68 | 67 | nrexdv 2842 |
. . . . . . 7
 


          |
69 | | lbsext.j |
. . . . . . . . . . . . . . . 16
LBasis   |
70 | | lbsext.c |
. . . . . . . . . . . . . . . 16

  |
71 | | lbsext.x |
. . . . . . . . . . . . . . . 16
 
          |
72 | | lbsext.p |
. . . . . . . . . . . . . . . 16
     |
73 | | lbsext.t |
. . . . . . . . . . . . . . . 16
          |
74 | 8, 69, 46, 28, 70, 71, 2, 72, 1, 22, 33, 73 | lbsextlem2 18375 |
. . . . . . . . . . . . . . 15
          |
75 | 74 | simpld 461 |
. . . . . . . . . . . . . 14
   |
76 | 8, 72 | lssss 18153 |
. . . . . . . . . . . . . 14
   |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13

  |
78 | 74 | simprd 465 |
. . . . . . . . . . . . 13
        |
79 | 8, 46 | lspss 18200 |
. . . . . . . . . . . . 13
      
     
          |
80 | 30, 77, 78, 79 | syl3anc 1267 |
. . . . . . . . . . . 12
     
          |
81 | 72, 46 | lspid 18198 |
. . . . . . . . . . . . 13
         |
82 | 30, 75, 81 | syl2anc 666 |
. . . . . . . . . . . 12
       |
83 | 80, 82 | sseqtrd 3467 |
. . . . . . . . . . 11
     
      |
84 | 83 | 3ad2ant1 1028 |
. . . . . . . . . 10
 

        
  |
85 | 84, 73 | syl6sseq 3477 |
. . . . . . . . 9
 

        
    
      |
86 | 85 | sseld 3430 |
. . . . . . . 8
 

     
   
    
       |
87 | | eliun 4282 |
. . . . . . . 8
     
   

          |
88 | 86, 87 | syl6ib 230 |
. . . . . . 7
 

     
    
           |
89 | 68, 88 | mtod 181 |
. . . . . 6
 

    
      |
90 | 89 | rexlimdv3a 2880 |
. . . . 5
  
            |
91 | 26, 90 | syl5bi 221 |
. . . 4
  
            |
92 | 91 | ralrimiv 2799 |
. . 3
              |
93 | 25, 92 | jca 535 |
. 2
                 |
94 | | sseq2 3453 |
. . . 4
       |
95 | | difeq1 3543 |
. . . . . . . 8
             |
96 | 95 | fveq2d 5867 |
. . . . . . 7
     
        
      |
97 | 96 | eleq2d 2513 |
. . . . . 6
          
            |
98 | 97 | notbid 296 |
. . . . 5
      
   
    
       |
99 | 98 | raleqbi1dv 2994 |
. . . 4
       
   
      
       |
100 | 94, 99 | anbi12d 716 |
. . 3
        
                      |
101 | 100, 2 | elrab2 3197 |
. 2
 
 
                  |
102 | 12, 93, 101 | sylanbrc 669 |
1
    |