Step | Hyp | Ref
| Expression |
1 | | exmidomniim 6718 |
. 2
EXMID 
Omni |
2 | | vex 2617 |
. . . . . . . . . 10
 |
3 | | eleq1w 2145 |
. . . . . . . . . 10
  Omni
Omni  |
4 | 2, 3 | spcv 2704 |
. . . . . . . . 9
 
Omni Omni |
5 | | xpeq1 4418 |
. . . . . . . . . . . . . 14
           |
6 | 5 | fveq1d 5258 |
. . . . . . . . . . . . 13
                   |
7 | 6 | eqeq1d 2093 |
. . . . . . . . . . . 12
                     |
8 | 7 | rexeqbi1dv 2566 |
. . . . . . . . . . 11
  
        
           |
9 | 6 | eqeq1d 2093 |
. . . . . . . . . . . 12
                     |
10 | 9 | raleqbi1dv 2565 |
. . . . . . . . . . 11
  
                    |
11 | 8, 10 | orbi12d 740 |
. . . . . . . . . 10
                     
 
        
            |
12 | | vex 2617 |
. . . . . . . . . . . . 13
 |
13 | | isomni 6713 |
. . . . . . . . . . . . 13
  Omni
             
         |
14 | 12, 13 | ax-mp 7 |
. . . . . . . . . . . 12
 Omni              
        |
15 | 14 | biimpi 118 |
. . . . . . . . . . 11
 Omni              
        |
16 | | 0ex 3934 |
. . . . . . . . . . . . . 14
 |
17 | 16 | prid1 3525 |
. . . . . . . . . . . . 13
    |
18 | | df2o3 6130 |
. . . . . . . . . . . . 13
    |
19 | 17, 18 | eleqtrri 2160 |
. . . . . . . . . . . 12
 |
20 | 19 | fconst6 5161 |
. . . . . . . . . . 11
         |
21 | | p0ex 3990 |
. . . . . . . . . . . . 13
   |
22 | 12, 21 | xpex 4514 |
. . . . . . . . . . . 12
     |
23 | | feq1 5101 |
. . . . . . . . . . . . 13
                     |
24 | | fveq1 5255 |
. . . . . . . . . . . . . . . 16
                   |
25 | 24 | eqeq1d 2093 |
. . . . . . . . . . . . . . 15
                     |
26 | 25 | rexbidv 2377 |
. . . . . . . . . . . . . 14
           
           |
27 | 24 | eqeq1d 2093 |
. . . . . . . . . . . . . . 15
                     |
28 | 27 | ralbidv 2376 |
. . . . . . . . . . . . . 14
                       |
29 | 26, 28 | orbi12d 740 |
. . . . . . . . . . . . 13
       
                                 |
30 | 23, 29 | imbi12d 232 |
. . . . . . . . . . . 12
            
    
     
                                 |
31 | 22, 30 | spcv 2704 |
. . . . . . . . . . 11
         
    
                
                     |
32 | 15, 20, 31 | mpisyl 1378 |
. . . . . . . . . 10
 Omni  
       

           |
33 | 11, 32 | vtoclga 2677 |
. . . . . . . . 9
 Omni  
       

           |
34 | 4, 33 | syl 14 |
. . . . . . . 8
 
Omni  
                    |
35 | 34 | adantr 270 |
. . . . . . 7
   Omni
  
 
        
           |
36 | | simplr 497 |
. . . . . . . . . 10
    Omni
   
             |
37 | | rexm 3365 |
. . . . . . . . . . . 12
             |
38 | | sssnm 3575 |
. . . . . . . . . . . 12
          |
39 | 37, 38 | syl 14 |
. . . . . . . . . . 11
          
 
     |
40 | 39 | adantl 271 |
. . . . . . . . . 10
    Omni
   
         
 
     |
41 | 36, 40 | mpbid 145 |
. . . . . . . . 9
    Omni
   
             |
42 | 41 | ex 113 |
. . . . . . . 8
   Omni
  
 
             |
43 | | nfv 1464 |
. . . . . . . . . . . 12
    Omni
    |
44 | | nfra1 2405 |
. . . . . . . . . . . 12
            |
45 | 43, 44 | nfan 1500 |
. . . . . . . . . . 11
    
Omni    
          |
46 | | nfcv 2225 |
. . . . . . . . . . 11
   |
47 | | nfcv 2225 |
. . . . . . . . . . 11
   |
48 | | 1n0 6132 |
. . . . . . . . . . . . . 14
 |
49 | 48 | neii 2253 |
. . . . . . . . . . . . 13
 |
50 | | simpr 108 |
. . . . . . . . . . . . . . . 16
    Omni
   
         
          |
51 | 50 | r19.21bi 2457 |
. . . . . . . . . . . . . . 15
    
Omni    
         
          |
52 | 16 | fvconst2 5456 |
. . . . . . . . . . . . . . . 16
           |
53 | 52 | adantl 271 |
. . . . . . . . . . . . . . 15
    
Omni    
         
          |
54 | 51, 53 | eqtr3d 2119 |
. . . . . . . . . . . . . 14
    
Omni    
         
  |
55 | 54 | ex 113 |
. . . . . . . . . . . . 13
    Omni
   
             |
56 | 49, 55 | mtoi 623 |
. . . . . . . . . . . 12
    Omni
   
        
  |
57 | 56 | pm2.21d 582 |
. . . . . . . . . . 11
    Omni
   
             |
58 | 45, 46, 47, 57 | ssrd 3017 |
. . . . . . . . . 10
    Omni
   
           |
59 | | ss0 3308 |
. . . . . . . . . 10

  |
60 | 58, 59 | syl 14 |
. . . . . . . . 9
    Omni
   
        
  |
61 | 60 | ex 113 |
. . . . . . . 8
   Omni
  
 
           |
62 | 42, 61 | orim12d 733 |
. . . . . . 7
   Omni
  
  
                 
       |
63 | 35, 62 | mpd 13 |
. . . . . 6
   Omni
  
      |
64 | 63 | orcomd 681 |
. . . . 5
   Omni
  
      |
65 | 64 | ex 113 |
. . . 4
 
Omni 
         |
66 | 65 | alrimiv 1799 |
. . 3
 
Omni             |
67 | | exmid01 3999 |
. . 3
EXMID
            |
68 | 66, 67 | sylibr 132 |
. 2
 
Omni
EXMID |
69 | 1, 68 | impbii 124 |
1
EXMID

Omni |