Step | Hyp | Ref
| Expression |
1 | | vdwmc.1 |
. . 3
 |
2 | | vdwmc.2 |
. . 3
   |
3 | | vdwmc.3 |
. . 3
       |
4 | 1, 2, 3 | vdwmc 14928 |
. 2
  MonoAP
  
   AP              |
5 | | vdwapid1 14925 |
. . . . . . . . . . . 12
 
   AP      |
6 | | ne0i 3737 |
. . . . . . . . . . . 12
   AP   
  AP      |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
 
   AP      |
8 | 7 | 3expb 1209 |
. . . . . . . . . 10
    
  AP      |
9 | 8 | adantll 720 |
. . . . . . . . 9
    
 
  AP      |
10 | | ssn0 3767 |
. . . . . . . . . 10
    AP             AP              |
11 | 10 | expcom 437 |
. . . . . . . . 9
   AP       AP                     |
12 | 9, 11 | syl 17 |
. . . . . . . 8
    
 
   AP                     |
13 | | disjsn 4032 |
. . . . . . . . . 10
    
  |
14 | 3 | adantr 467 |
. . . . . . . . . . . 12
 

      |
15 | | fimacnvdisj 5761 |
. . . . . . . . . . . . 13
      
             |
16 | 15 | ex 436 |
. . . . . . . . . . . 12
                    |
17 | 14, 16 | syl 17 |
. . . . . . . . . . 11
 

               |
18 | 17 | adantr 467 |
. . . . . . . . . 10
    
 
               |
19 | 13, 18 | syl5bir 222 |
. . . . . . . . 9
    
 

          |
20 | 19 | necon1ad 2641 |
. . . . . . . 8
    
 
           |
21 | 12, 20 | syld 45 |
. . . . . . 7
    
 
   AP              |
22 | 21 | rexlimdvva 2886 |
. . . . . 6
 

  
  AP              |
23 | 22 | pm4.71rd 641 |
. . . . 5
 

  
  AP          

    AP   
           |
24 | 23 | exbidv 1768 |
. . . 4
 

       AP   
          
   AP   
           |
25 | | df-rex 2743 |
. . . 4
  
   AP   
          
   AP   
          |
26 | 24, 25 | syl6bbr 267 |
. . 3
 

       AP   
        
   AP              |
27 | | vdwmc2.4 |
. . . . . . . . 9
   |
28 | 3, 27 | ffvelrnd 6023 |
. . . . . . . 8
       |
29 | | ne0i 3737 |
. . . . . . . 8
       |
30 | 28, 29 | syl 17 |
. . . . . . 7
   |
31 | 30 | adantr 467 |
. . . . . 6
 
   |
32 | | 1nn 10620 |
. . . . . . . . 9
 |
33 | 32 | ne0ii 3738 |
. . . . . . . 8
 |
34 | | simpllr 769 |
. . . . . . . . . . . . . . 15
   
     |
35 | 34 | fveq2d 5869 |
. . . . . . . . . . . . . 14
   
   AP  AP    |
36 | 35 | oveqd 6307 |
. . . . . . . . . . . . 13
   
     AP      AP      |
37 | | vdwap0 14926 |
. . . . . . . . . . . . . 14
 
   AP      |
38 | 37 | adantll 720 |
. . . . . . . . . . . . 13
   
     AP      |
39 | 36, 38 | eqtrd 2485 |
. . . . . . . . . . . 12
   
     AP      |
40 | | 0ss 3763 |
. . . . . . . . . . . 12
        |
41 | 39, 40 | syl6eqss 3482 |
. . . . . . . . . . 11
   
     AP   
         |
42 | 41 | ralrimiva 2802 |
. . . . . . . . . 10
   
    AP             |
43 | | r19.2z 3858 |
. . . . . . . . . 10
  
  AP            
  AP             |
44 | 33, 42, 43 | sylancr 669 |
. . . . . . . . 9
   
    AP             |
45 | 44 | ralrimiva 2802 |
. . . . . . . 8
 
     AP   
         |
46 | | r19.2z 3858 |
. . . . . . . 8
  
   AP   
            AP   
         |
47 | 33, 45, 46 | sylancr 669 |
. . . . . . 7
 
     AP   
         |
48 | 47 | ralrimivw 2803 |
. . . . . 6
 
 
    AP   
         |
49 | | r19.2z 3858 |
. . . . . 6
  

   AP   
        
    AP   
         |
50 | 31, 48, 49 | syl2anc 667 |
. . . . 5
 
 
    AP   
         |
51 | | rexex 2844 |
. . . . 5
  
   AP   
      
  
   AP             |
52 | 50, 51 | syl 17 |
. . . 4
 
   
   AP             |
53 | 52, 50 | 2thd 244 |
. . 3
 
        AP   
        
   AP              |
54 | | elnn0 10871 |
. . . 4

    |
55 | 2, 54 | sylib 200 |
. . 3
 
   |
56 | 26, 53, 55 | mpjaodan 795 |
. 2
     
  AP          

    AP   
          |
57 | | vdwapval 14923 |
. . . . . . . . 9
 
    AP   
    
          |
58 | 57 | 3expb 1209 |
. . . . . . . 8
    
   AP    
              |
59 | 2, 58 | sylan 474 |
. . . . . . 7
 
      AP   
    
          |
60 | 59 | imbi1d 319 |
. . . . . 6
 
       AP           
 
                      |
61 | 60 | albidv 1767 |
. . . . 5
 
         AP                                      |
62 | | dfss2 3421 |
. . . . 5
   AP          
     AP   
          |
63 | | ralcom4 3066 |
. . . . . 6
 
             
       
  
           
          |
64 | | ovex 6318 |
. . . . . . . 8
     |
65 | | eleq1 2517 |
. . . . . . . 8
            
              |
66 | 64, 65 | ceqsalv 3075 |
. . . . . . 7
       
       
             |
67 | 66 | ralbii 2819 |
. . . . . 6
 
             
       
    
                |
68 | | r19.23v 2867 |
. . . . . . 7
 
           
       
 
                     |
69 | 68 | albii 1691 |
. . . . . 6
                       
       
                 |
70 | 63, 67, 69 | 3bitr3i 279 |
. . . . 5
 
                         
                 |
71 | 61, 62, 70 | 3bitr4g 292 |
. . . 4
 
      AP   
                             |
72 | 71 | 2rexbidva 2907 |
. . 3
      AP   
         
                     |
73 | 72 | rexbidv 2901 |
. 2
       AP   
        
 
                     |
74 | 4, 56, 73 | 3bitrd 283 |
1
  MonoAP

      
                 |