Step | Hyp | Ref
| Expression |
1 | | orc 391 |
. . . . 5
                     |
2 | 1 | a1d 26 |
. . . 4
   
                       |
3 | | eliun 4296 |
. . . . . . . . . 10
        
        |
4 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    |
5 | 4 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

     |
6 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

  
  |
7 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

     |
8 | | otthg 4698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
               |
9 | 5, 6, 7, 8 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

                 |
10 | | simp1 1014 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
11 | 9, 10 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . 22
  

               |
12 | 11 | con3d 140 |
. . . . . . . . . . . . . . . . . . . . 21
  

   
           |
13 | 12 | ex 440 |
. . . . . . . . . . . . . . . . . . . 20
   
  
            |
14 | 13 | com13 83 |
. . . . . . . . . . . . . . . . . . 19
                   |
15 | 14 | imp31 438 |
. . . . . . . . . . . . . . . . . 18
    
              |
16 | 15 | adantr 471 |
. . . . . . . . . . . . . . . . 17
   


  

                 |
17 | 16 | adantr 471 |
. . . . . . . . . . . . . . . 16
     

  

                  |
18 | | elsn 3993 |
. . . . . . . . . . . . . . . . . . 19
             |
19 | | eqeq1 2465 |
. . . . . . . . . . . . . . . . . . . 20
                     |
20 | 19 | notbid 300 |
. . . . . . . . . . . . . . . . . . 19
     
               |
21 | 18, 20 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
           
           |
22 | 21 | adantl 472 |
. . . . . . . . . . . . . . . . 17
   


  

       
               |
23 | 22 | adantr 471 |
. . . . . . . . . . . . . . . 16
     

  

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

  

       
      |
25 | | elsn 3993 |
. . . . . . . . . . . . . . 15
             |
26 | 24, 25 | sylnibr 311 |
. . . . . . . . . . . . . 14
     

  

       
        |
27 | 26 | nrexdv 2854 |
. . . . . . . . . . . . 13
   


  

                |
28 | | eliun 4296 |
. . . . . . . . . . . . 13
        
        |
29 | 27, 28 | sylnibr 311 |
. . . . . . . . . . . 12
   


  

      
         |
30 | 29 | ex 440 |
. . . . . . . . . . 11
    
          
          |
31 | 30 | rexlimdva 2890 |
. . . . . . . . . 10
        
     
          |
32 | 3, 31 | syl5bi 225 |
. . . . . . . . 9
               
         |
33 | 32 | ralrimiv 2811 |
. . . . . . . 8
       
               |
34 | | oteq3 4190 |
. . . . . . . . . . . . 13
           |
35 | 34 | sneqd 3991 |
. . . . . . . . . . . 12
               |
36 | 35 | cbviunv 4330 |
. . . . . . . . . . 11

     
        |
37 | 36 | eleq2i 2531 |
. . . . . . . . . 10
        
        |
38 | 37 | notbii 302 |
. . . . . . . . 9
 
      
        |
39 | 38 | ralbii 2830 |
. . . . . . . 8
 
      
     
      
         |
40 | 33, 39 | sylibr 217 |
. . . . . . 7
       
               |
41 | | disj 3816 |
. . . . . . 7
                 
               |
42 | 40, 41 | sylibr 217 |
. . . . . 6
        
                |
43 | 42 | olcd 399 |
. . . . 5
         
      
          |
44 | 43 | ex 440 |
. . . 4
        
                  |
45 | 2, 44 | pm2.61i 169 |
. . 3
  
                      |
46 | 45 | ralrimivva 2820 |
. 2
 


 
                 |
47 | | oteq1 4188 |
. . . . 5
           |
48 | 47 | sneqd 3991 |
. . . 4
               |
49 | 48 | iuneq2d 4318 |
. . 3
 
     
         |
50 | 49 | disjor 4400 |
. 2
Disj
        
  
                 |
51 | 46, 50 | sylibr 217 |
1
 Disj          |