Step | Hyp | Ref
| Expression |
1 | | 0ex 4535 |
. . . . 5
 |
2 | 1 | prid1 4080 |
. . . 4
    |
3 | 2 | a1i 11 |
. . 3
      |
4 | 1 | a1i 11 |
. . . . . . . . 9
   |
5 | | id 22 |
. . . . . . . . 9
   |
6 | | uniprg 4212 |
. . . . . . . . 9
 
         |
7 | 4, 5, 6 | syl2anc 667 |
. . . . . . . 8
         |
8 | | uncom 3578 |
. . . . . . . . . 10
     |
9 | | un0 3759 |
. . . . . . . . . 10
   |
10 | 8, 9 | eqtri 2473 |
. . . . . . . . 9
   |
11 | 10 | a1i 11 |
. . . . . . . 8
     |
12 | | eqidd 2452 |
. . . . . . . 8
   |
13 | 7, 11, 12 | 3eqtrd 2489 |
. . . . . . 7
       |
14 | 13 | difeq1d 3550 |
. . . . . 6
           |
15 | 14 | adantr 467 |
. . . . 5
 
              |
16 | | difeq2 3545 |
. . . . . . . . . 10

      |
17 | 16 | adantl 468 |
. . . . . . . . 9
 
       |
18 | | dif0 3837 |
. . . . . . . . . 10
   |
19 | 18 | a1i 11 |
. . . . . . . . 9
 
     |
20 | 17, 19 | eqtrd 2485 |
. . . . . . . 8
 
     |
21 | | prid2g 4079 |
. . . . . . . . 9
      |
22 | 21 | adantr 467 |
. . . . . . . 8
 

     |
23 | 20, 22 | eqeltrd 2529 |
. . . . . . 7
 
        |
24 | 23 | adantlr 721 |
. . . . . 6
  
   
        |
25 | | simpll 760 |
. . . . . . 7
  
   

  |
26 | | simpl 459 |
. . . . . . . . 9
    
      |
27 | | neqne 37374 |
. . . . . . . . . 10
   |
28 | 27 | adantl 468 |
. . . . . . . . 9
    
   |
29 | | elprn1 37713 |
. . . . . . . . 9
        |
30 | 26, 28, 29 | syl2anc 667 |
. . . . . . . 8
    
   |
31 | 30 | adantll 720 |
. . . . . . 7
  
   
   |
32 | | difeq2 3545 |
. . . . . . . . . 10
       |
33 | | difid 3835 |
. . . . . . . . . . 11
   |
34 | 33 | a1i 11 |
. . . . . . . . . 10
     |
35 | 32, 34 | eqtrd 2485 |
. . . . . . . . 9
     |
36 | 2 | a1i 11 |
. . . . . . . . 9
      |
37 | 35, 36 | eqeltrd 2529 |
. . . . . . . 8
        |
38 | 37 | adantl 468 |
. . . . . . 7
 
        |
39 | 25, 31, 38 | syl2anc 667 |
. . . . . 6
  
   
        |
40 | 24, 39 | pm2.61dan 800 |
. . . . 5
 
           |
41 | 15, 40 | eqeltrd 2529 |
. . . 4
 
               |
42 | 41 | ralrimiva 2802 |
. . 3
                |
43 | | elpwi 3960 |
. . . . . . . . . . . . 13
          |
44 | | uniss 4219 |
. . . . . . . . . . . . 13
           |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . 12
            |
46 | 45 | adantl 468 |
. . . . . . . . . . 11
 
     
      |
47 | 13 | adantr 467 |
. . . . . . . . . . 11
 
           |
48 | 46, 47 | sseqtrd 3468 |
. . . . . . . . . 10
 
     
  |
49 | 48 | adantr 467 |
. . . . . . . . 9
  
    
    |
50 | | elssuni 4227 |
. . . . . . . . . 10
    |
51 | 50 | adantl 468 |
. . . . . . . . 9
  
    
    |
52 | 49, 51 | jca 535 |
. . . . . . . 8
  
    
  
    |
53 | | eqss 3447 |
. . . . . . . 8
 
      |
54 | 52, 53 | sylibr 216 |
. . . . . . 7
  
    
    |
55 | 21 | ad2antrr 732 |
. . . . . . 7
  
    
      |
56 | 54, 55 | eqeltrd 2529 |
. . . . . 6
  
    
       |
57 | | id 22 |
. . . . . . . . . . . 12
           |
58 | | pwpr 4194 |
. . . . . . . . . . . 12
                    |
59 | 57, 58 | syl6eleq 2539 |
. . . . . . . . . . 11
                      |
60 | 59 | adantr 467 |
. . . . . . . . . 10
     

                 |
61 | 60 | adantll 720 |
. . . . . . . . 9
  
    
                  |
62 | | snidg 3994 |
. . . . . . . . . . . . . . . 16
     |
63 | 62 | adantr 467 |
. . . . . . . . . . . . . . 15
 
       |
64 | | id 22 |
. . . . . . . . . . . . . . . . 17
       |
65 | 64 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
       |
66 | 65 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
  |
67 | 63, 66 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
 
     |
68 | 67 | adantlr 721 |
. . . . . . . . . . . . 13
  
              |
69 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . 14
  
              |
70 | | simpl 459 |
. . . . . . . . . . . . . . . 16
         
             |
71 | 64 | necon3bi 2650 |
. . . . . . . . . . . . . . . . 17
       |
72 | 71 | adantl 468 |
. . . . . . . . . . . . . . . 16
         
       |
73 | | elprn1 37713 |
. . . . . . . . . . . . . . . 16
            
     |
74 | 70, 72, 73 | syl2anc 667 |
. . . . . . . . . . . . . . 15
         
        |
75 | 74 | adantll 720 |
. . . . . . . . . . . . . 14
  
                 |
76 | 21 | adantr 467 |
. . . . . . . . . . . . . . 15
 
         |
77 | | id 22 |
. . . . . . . . . . . . . . . . 17
         |
78 | 77 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
      
  |
79 | 78 | adantl 468 |
. . . . . . . . . . . . . . 15
 
         |
80 | 76, 79 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
 
      |
81 | 69, 75, 80 | syl2anc 667 |
. . . . . . . . . . . . 13
  
              |
82 | 68, 81 | pm2.61dan 800 |
. . . . . . . . . . . 12
 
   
       |
83 | 82 | adantlr 721 |
. . . . . . . . . . 11
               |
84 | | simplr 762 |
. . . . . . . . . . 11
            
  |
85 | 83, 84 | pm2.65da 580 |
. . . . . . . . . 10
 

          |
86 | 85 | adantlr 721 |
. . . . . . . . 9
  
    

   
      |
87 | | elunnel2 37360 |
. . . . . . . . 9
    
           
   
            |
88 | 61, 86, 87 | syl2anc 667 |
. . . . . . . 8
  
    
        |
89 | | unieq 4206 |
. . . . . . . . . . 11

    |
90 | | uni0 4225 |
. . . . . . . . . . . 12
  |
91 | 90 | a1i 11 |
. . . . . . . . . . 11

   |
92 | 89, 91 | eqtrd 2485 |
. . . . . . . . . 10

   |
93 | 92 | adantl 468 |
. . . . . . . . 9
      
 
  |
94 | | simpl 459 |
. . . . . . . . . . 11
      
        |
95 | 27 | adantl 468 |
. . . . . . . . . . 11
      
   |
96 | | elprn1 37713 |
. . . . . . . . . . 11
            |
97 | 94, 95, 96 | syl2anc 667 |
. . . . . . . . . 10
      
     |
98 | | unieq 4206 |
. . . . . . . . . . 11
         |
99 | 1 | unisn 4213 |
. . . . . . . . . . . 12
    |
100 | 99 | a1i 11 |
. . . . . . . . . . 11
        |
101 | 98, 100 | eqtrd 2485 |
. . . . . . . . . 10
      |
102 | 97, 101 | syl 17 |
. . . . . . . . 9
      
 
  |
103 | 93, 102 | pm2.61dan 800 |
. . . . . . . 8
         |
104 | 88, 103 | syl 17 |
. . . . . . 7
  
    
    |
105 | 2 | a1i 11 |
. . . . . . 7
  
    
      |
106 | 104, 105 | eqeltrd 2529 |
. . . . . 6
  
    
       |
107 | 56, 106 | pm2.61dan 800 |
. . . . 5
 
     
     |
108 | 107 | a1d 26 |
. . . 4
 
             |
109 | 108 | ralrimiva 2802 |
. . 3
             |
110 | 3, 42, 109 | 3jca 1188 |
. 2
                  
   
        |
111 | | prex 4642 |
. . . 4
    |
112 | 111 | a1i 11 |
. . 3
      |
113 | | issal 38175 |
. . 3
  

    SAlg                  
   
         |
114 | 112, 113 | syl 17 |
. 2
     SAlg     
                
         |
115 | 110, 114 | mpbird 236 |
1
    SAlg |