Step | Hyp | Ref
| Expression |
1 | | df-disj 3981 |
. . . 4
Disj
  
  |
2 | | elin 3318 |
. . . . . . . . . 10
  
    
   |
3 | | eliun 3890 |
. . . . . . . . . . 11
 

  |
4 | | eliun 3890 |
. . . . . . . . . . 11
 

  |
5 | 3, 4 | anbi12i 460 |
. . . . . . . . . 10
  
 
 

   |
6 | 2, 5 | bitri 184 |
. . . . . . . . 9
  
   
    |
7 | | nfv 1528 |
. . . . . . . . . . . 12

 |
8 | 7 | rmo3 3054 |
. . . . . . . . . . 11
 


    ![] ]](rbrack.gif)     |
9 | | simprl 529 |
. . . . . . . . . . . . . 14
         ![] ]](rbrack.gif)       
   
  |
10 | | nfv 1528 |
. . . . . . . . . . . . . . 15

 |
11 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
12 | 11 | nfcri 2313 |
. . . . . . . . . . . . . . 15

  ![]_ ]_](_urbrack.gif)  |
13 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
14 | 13 | eleq2d 2247 |
. . . . . . . . . . . . . . 15
 
  ![]_ ]_](_urbrack.gif)    |
15 | 10, 12, 14 | cbvrex 2700 |
. . . . . . . . . . . . . 14
 

  ![]_ ]_](_urbrack.gif)   |
16 | 9, 15 | sylib 122 |
. . . . . . . . . . . . 13
         ![] ]](rbrack.gif)       
   
  ![]_ ]_](_urbrack.gif)   |
17 | | simplrr 536 |
. . . . . . . . . . . . . . 15
    

    ![] ]](rbrack.gif)       
      ![]_ ]_](_urbrack.gif)   
  |
18 | | nfv 1528 |
. . . . . . . . . . . . . . . 16
  |
19 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)  |
20 | 19 | nfcri 2313 |
. . . . . . . . . . . . . . . 16

  ![]_ ]_](_urbrack.gif)  |
21 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
22 | 21 | eleq2d 2247 |
. . . . . . . . . . . . . . . 16
 
  ![]_ ]_](_urbrack.gif)    |
23 | 18, 20, 22 | cbvrex 2700 |
. . . . . . . . . . . . . . 15
 

  ![]_ ]_](_urbrack.gif)   |
24 | 17, 23 | sylib 122 |
. . . . . . . . . . . . . 14
    

    ![] ]](rbrack.gif)       
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)   |
25 | | simplrl 535 |
. . . . . . . . . . . . . . 15
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
26 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . 20
   
    ![] ]](rbrack.gif)        |
27 | 26 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . 19
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
28 | 27, 25 | sseldd 3156 |
. . . . . . . . . . . . . . . . . 18
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
29 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . 20
   
    ![] ]](rbrack.gif)        |
30 | 29 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . 19
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
31 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
32 | 30, 31 | sseldd 3156 |
. . . . . . . . . . . . . . . . . 18
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
33 | 28, 32 | jca 306 |
. . . . . . . . . . . . . . . . 17
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  

   |
34 | | simp-4l 541 |
. . . . . . . . . . . . . . . . 17
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  


    ![] ]](rbrack.gif)     |
35 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)   |
36 | | simprr 531 |
. . . . . . . . . . . . . . . . . . 19
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)   |
37 | 20, 22 | sbie 1791 |
. . . . . . . . . . . . . . . . . . 19
   ![] ]](rbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
38 | 36, 37 | sylibr 134 |
. . . . . . . . . . . . . . . . . 18
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  ![] ]](rbrack.gif)   |
39 | 35, 38 | jca 306 |
. . . . . . . . . . . . . . . . 17
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif)    |
40 | | nfs1v 1939 |
. . . . . . . . . . . . . . . . . . . 20
  
 ![] ]](rbrack.gif)  |
41 | 12, 40 | nfan 1565 |
. . . . . . . . . . . . . . . . . . 19
     ![]_ ]_](_urbrack.gif)   ![] ]](rbrack.gif)   |
42 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . 19

 |
43 | 41, 42 | nfim 1572 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif)    |
44 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif) 
  |
45 | 14 | anbi1d 465 |
. . . . . . . . . . . . . . . . . . 19
     ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif)     |
46 | | equequ1 1712 |
. . . . . . . . . . . . . . . . . . 19
 
   |
47 | 45, 46 | imbi12d 234 |
. . . . . . . . . . . . . . . . . 18
      ![] ]](rbrack.gif)  
    ![]_ ]_](_urbrack.gif)   ![] ]](rbrack.gif)      |
48 | | sbequ 1840 |
. . . . . . . . . . . . . . . . . . . 20
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
49 | 48 | anbi2d 464 |
. . . . . . . . . . . . . . . . . . 19
     ![]_ ]_](_urbrack.gif)   ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif)     |
50 | | equequ2 1713 |
. . . . . . . . . . . . . . . . . . 19
 
   |
51 | 49, 50 | imbi12d 234 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)
  ![] ]](rbrack.gif)  
    ![]_ ]_](_urbrack.gif)   ![] ]](rbrack.gif)      |
52 | 43, 44, 47, 51 | rspc2 2852 |
. . . . . . . . . . . . . . . . 17
 
        ![] ]](rbrack.gif)  
    ![]_ ]_](_urbrack.gif)   ![] ]](rbrack.gif)      |
53 | 33, 34, 39, 52 | syl3c 63 |
. . . . . . . . . . . . . . . 16
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
54 | 53, 31 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
  |
55 | | inelcm 3483 |
. . . . . . . . . . . . . . 15
 
     |
56 | 25, 54, 55 | syl2anc 411 |
. . . . . . . . . . . . . 14
     

    ![] ]](rbrack.gif) 
     
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)  
    |
57 | 24, 56 | rexlimddv 2599 |
. . . . . . . . . . . . 13
    

    ![] ]](rbrack.gif)       
      ![]_ ]_](_urbrack.gif)       |
58 | 16, 57 | rexlimddv 2599 |
. . . . . . . . . . . 12
         ![] ]](rbrack.gif)       
       |
59 | 58 | exp31 364 |
. . . . . . . . . . 11
 

    ![] ]](rbrack.gif) 
  
    
       |
60 | 8, 59 | sylbi 121 |
. . . . . . . . . 10
   
    
       |
61 | 60 | impcom 125 |
. . . . . . . . 9
  
  
  
       |
62 | 6, 61 | biimtrid 152 |
. . . . . . . 8
  
  
   

     |
63 | 62 | necon2bd 2405 |
. . . . . . 7
  
  
  
       |
64 | 63 | impancom 260 |
. . . . . 6
  
             |
65 | 64 | 3impa 1194 |
. . . . 5
 
  
 
 
     |
66 | 65 | alimdv 1879 |
. . . 4
 
  
   
   
    |
67 | 1, 66 | biimtrid 152 |
. . 3
 
  
Disj
   
    |
68 | 67 | impcom 125 |
. 2
 Disj


   
  
   |
69 | | eq0 3441 |
. 2
            |
70 | 68, 69 | sylibr 134 |
1
 Disj


         |