Step | Hyp | Ref
| Expression |
1 | | opelxp 4317 |
. . 3
      
   |
2 | | vex 2554 |
. . . . . . 7
 |
3 | 2 | elima2 4617 |
. . . . . 6

~Q0       
  ~Q0    |
4 | | elxp 4305 |
. . . . . . . . . 10
  
             |
5 | 4 | anbi1i 431 |
. . . . . . . . 9
    ~Q0           
  ~Q0    |
6 | | 19.41vv 1780 |
. . . . . . . . 9
         

  ~Q0             
~Q0    |
7 | 5, 6 | bitr4i 176 |
. . . . . . . 8
    ~Q0           
  ~Q0    |
8 | | simplr 482 |
. . . . . . . . . . 11
      
  ~Q0      |
9 | | breq1 3758 |
. . . . . . . . . . . . 13
    
~Q0    ~Q0    |
10 | 9 | adantr 261 |
. . . . . . . . . . . 12
    

  
~Q0    ~Q0    |
11 | 10 | biimpa 280 |
. . . . . . . . . . 11
      
  ~Q0    
~Q0   |
12 | | id 19 |
. . . . . . . . . . . 12
       ~Q0       
~Q0    |
13 | | enq0er 6418 |
. . . . . . . . . . . . . . 15
~Q0    |
14 | 13 | a1i 9 |
. . . . . . . . . . . . . 14
       ~Q0  ~Q0     |
15 | | simpr 103 |
. . . . . . . . . . . . . 14
       ~Q0     ~Q0   |
16 | 14, 15 | ercl2 6055 |
. . . . . . . . . . . . 13
       ~Q0      |
17 | | elxp 4305 |
. . . . . . . . . . . . 13
  
             |
18 | 16, 17 | sylib 127 |
. . . . . . . . . . . 12
       ~Q0          
    |
19 | | 19.42vv 1785 |
. . . . . . . . . . . 12
            ~Q0         
  
    ~Q0          
     |
20 | 12, 18, 19 | sylanbrc 394 |
. . . . . . . . . . 11
       ~Q0            
~Q0  
  
      |
21 | 8, 11, 20 | syl2anc 391 |
. . . . . . . . . 10
      
  ~Q0        
    ~Q0            |
22 | | simprrl 491 |
. . . . . . . . . . . . 13
   

  
~Q0  
  
      |
23 | | elni 6292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
24 | 23 | simprbi 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
25 | 24 | neneqd 2221 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
26 | 25 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
27 | | elni 6292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
28 | 27 | simprbi 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
29 | 28 | neneqd 2221 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
30 | 29 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
31 | 26, 30 | jca 290 |
. . . . . . . . . . . . . . . . . . . . 21
           |
32 | | pm4.56 805 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
   |
33 | 31, 32 | sylib 127 |
. . . . . . . . . . . . . . . . . . . 20
       
   |
34 | | pinn 6293 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
35 | 34 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . . . 21
         |
36 | | pinn 6293 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
37 | 36 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . . . 21
         |
38 | | nnm00 6038 |
. . . . . . . . . . . . . . . . . . . . 21
 
   

    |
39 | 35, 37, 38 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . . 20
               |
40 | 33, 39 | mtbird 597 |
. . . . . . . . . . . . . . . . . . 19
           |
41 | 40 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . . 18
   

  
~Q0  
  
     
  |
42 | | breq2 3759 |
. . . . . . . . . . . . . . . . . . . . . 22
       
~Q0    ~Q0       |
43 | 42 | biimpac 282 |
. . . . . . . . . . . . . . . . . . . . 21
     ~Q0
      
~Q0      |
44 | 43 | ad2ant2lr 479 |
. . . . . . . . . . . . . . . . . . . 20
   

  
~Q0  
  
       ~Q0      |
45 | | enq0breq 6419 |
. . . . . . . . . . . . . . . . . . . . . 22
          
~Q0           |
46 | 34, 45 | sylanl1 382 |
. . . . . . . . . . . . . . . . . . . . 21
          
~Q0           |
47 | 46 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . . . . 20
   

  
~Q0  
  
        ~Q0           |
48 | 44, 47 | mpbid 135 |
. . . . . . . . . . . . . . . . . . 19
   

  
~Q0  
  
     
    |
49 | 48 | eqeq1d 2045 |
. . . . . . . . . . . . . . . . . 18
   

  
~Q0  
  
      
     |
50 | 41, 49 | mtbid 596 |
. . . . . . . . . . . . . . . . 17
   

  
~Q0  
  
     
  |
51 | | pinn 6293 |
. . . . . . . . . . . . . . . . . . . 20
   |
52 | | nnm00 6038 |
. . . . . . . . . . . . . . . . . . . 20
 
   

    |
53 | 51, 52 | sylan 267 |
. . . . . . . . . . . . . . . . . . 19
 
   

    |
54 | 53 | ad2ant2lr 479 |
. . . . . . . . . . . . . . . . . 18
               |
55 | 54 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . 17
   

  
~Q0  
  
      

    |
56 | 50, 55 | mtbid 596 |
. . . . . . . . . . . . . . . 16
   

  
~Q0  
  
        |
57 | | pm4.56 805 |
. . . . . . . . . . . . . . . 16
 
 
   |
58 | 56, 57 | sylibr 137 |
. . . . . . . . . . . . . . 15
   

  
~Q0  
  
        |
59 | 58 | simprd 107 |
. . . . . . . . . . . . . 14
   

  
~Q0  
  
      |
60 | 59 | neneqad 2278 |
. . . . . . . . . . . . 13
   

  
~Q0  
  
      |
61 | | elni 6292 |
. . . . . . . . . . . . 13
     |
62 | 22, 60, 61 | sylanbrc 394 |
. . . . . . . . . . . 12
   

  
~Q0  
  
      |
63 | | simprrr 492 |
. . . . . . . . . . . 12
   

  
~Q0  
  
      |
64 | | eleq1 2097 |
. . . . . . . . . . . . . 14
               |
65 | | opelxp 4317 |
. . . . . . . . . . . . . 14
      
   |
66 | 64, 65 | syl6bb 185 |
. . . . . . . . . . . . 13
            |
67 | 66 | ad2antrl 459 |
. . . . . . . . . . . 12
   

  
~Q0  
  
       
    |
68 | 62, 63, 67 | mpbir2and 850 |
. . . . . . . . . . 11
   

  
~Q0  
  
        |
69 | 68 | exlimivv 1773 |
. . . . . . . . . 10
            ~Q0         
    |
70 | 21, 69 | syl 14 |
. . . . . . . . 9
      
  ~Q0      |
71 | 70 | exlimivv 1773 |
. . . . . . . 8
         

  ~Q0      |
72 | 7, 71 | sylbi 114 |
. . . . . . 7
    ~Q0      |
73 | 72 | exlimiv 1486 |
. . . . . 6
     
~Q0      |
74 | 3, 73 | sylbi 114 |
. . . . 5

~Q0         |
75 | 74 | ssriv 2943 |
. . . 4
~Q0        |
76 | | ecinxp 6117 |
. . . 4
  ~Q0    
            
~Q0      ![]](rbrack.gif)
~Q0          |
77 | 75, 76 | mpan 400 |
. . 3
           ~Q0      ![]](rbrack.gif)
~Q0          |
78 | 1, 77 | sylbir 125 |
. 2
 
      ~Q0      ![]](rbrack.gif)
~Q0          |
79 | | enq0enq 6414 |
. . 3
~Q0   
     |
80 | | eceq2 6079 |
. . 3
~Q0                  ![]](rbrack.gif)
~Q0          |
81 | 79, 80 | ax-mp 7 |
. 2
          ![]](rbrack.gif)
~Q0         |
82 | 78, 81 | syl6eqr 2087 |
1
 
      ~Q0       |