Step | Hyp | Ref
| Expression |
1 | | orc 387 |
. . . . 5
               
               |
2 | 1 | a1d 26 |
. . . 4
   
                
                |
3 | | eliun 4283 |
. . . . . . . . . 10
            
              |
4 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    |
5 | 4 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
     |
6 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
     |
7 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
         |
8 | | otthg 4685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
    
    
    |
9 | 5, 6, 7, 8 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
            
    |
10 | | simp1 1008 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
11 | 9, 10 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . 22
       
               |
12 | 11 | con3d 139 |
. . . . . . . . . . . . . . . . . . . . 21
       
   
           |
13 | 12 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
       
 

            |
14 | 13 | com13 83 |
. . . . . . . . . . . . . . . . . . 19
                       |
15 | 14 | imp31 434 |
. . . . . . . . . . . . . . . . . 18
    
       
          |
16 | 15 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   


  
           
          |
17 | 16 | adantr 467 |
. . . . . . . . . . . . . . . 16
     

  
                           |
18 | | elsn 3982 |
. . . . . . . . . . . . . . . . . . 19
             |
19 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . . 20
                     |
20 | 19 | notbid 296 |
. . . . . . . . . . . . . . . . . . 19
     
               |
21 | 18, 20 | sylbi 199 |
. . . . . . . . . . . . . . . . . 18
           
           |
22 | 21 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   


  
                
           |
23 | 22 | adantr 467 |
. . . . . . . . . . . . . . . 16
     

  
                                 |
24 | 17, 23 | mpbird 236 |
. . . . . . . . . . . . . . 15
     

  
                
      |
25 | | elsn 3982 |
. . . . . . . . . . . . . . 15
             |
26 | 24, 25 | sylnibr 307 |
. . . . . . . . . . . . . 14
     

  
                
        |
27 | 26 | nrexdv 2843 |
. . . . . . . . . . . . 13
   


  
           
              |
28 | | eliun 4283 |
. . . . . . . . . . . . 13
            
              |
29 | 27, 28 | sylnibr 307 |
. . . . . . . . . . . 12
   


  
           
              |
30 | 29 | ex 436 |
. . . . . . . . . . 11
    
                              |
31 | 30 | rexlimdva 2879 |
. . . . . . . . . 10
                   
               |
32 | 3, 31 | syl5bi 221 |
. . . . . . . . 9
                   
               |
33 | 32 | ralrimiv 2800 |
. . . . . . . 8
       
          
              |
34 | | oteq3 4177 |
. . . . . . . . . . . . 13
           |
35 | 34 | sneqd 3980 |
. . . . . . . . . . . 12
               |
36 | 35 | cbviunv 4317 |
. . . . . . . . . . 11
            
            |
37 | 36 | eleq2i 2521 |
. . . . . . . . . 10
            
              |
38 | 37 | notbii 298 |
. . . . . . . . 9
            
              |
39 | 38 | ralbii 2819 |
. . . . . . . 8
 
                       
          
              |
40 | 33, 39 | sylibr 216 |
. . . . . . 7
       
          
              |
41 | | disj 3805 |
. . . . . . 7
                           
          
              |
42 | 40, 41 | sylibr 216 |
. . . . . 6
                    
              |
43 | 42 | olcd 395 |
. . . . 5
         
                           |
44 | 43 | ex 436 |
. . . 4
                    
                |
45 | 2, 44 | pm2.61i 168 |
. . 3
  
                
               |
46 | 45 | ralrimivva 2809 |
. 2
 


 
                           |
47 | | sneq 3978 |
. . . . 5
       |
48 | 47 | difeq2d 3551 |
. . . 4
           |
49 | | oteq1 4175 |
. . . . 5
           |
50 | 49 | sneqd 3980 |
. . . 4
               |
51 | 48, 50 | iuneq12d 4304 |
. . 3
             
             |
52 | 51 | disjor 4387 |
. 2
Disj
           



 
                           |
53 | 46, 52 | sylibr 216 |
1
 Disj               |