Step | Hyp | Ref
| Expression |
1 | | cfval 8091 |
. . . 4
             
 

     |
2 | 1 | eqeq1d 2420 |
. . 3
     
        
 

      |
3 | | vex 2927 |
. . . . . . . . 9
 |
4 | | eqeq1 2418 |
. . . . . . . . . . 11
     
       |
5 | 4 | anbi1d 686 |
. . . . . . . . . 10
         
      
 

     |
6 | 5 | exbidv 1633 |
. . . . . . . . 9
        
 

 
         
     |
7 | 3, 6 | elab 3050 |
. . . . . . . 8
        
 

         
 

    |
8 | | fveq2 5695 |
. . . . . . . . . . . 12
    
              |
9 | | cardidm 7810 |
. . . . . . . . . . . 12
             |
10 | 8, 9 | syl6eq 2460 |
. . . . . . . . . . 11
    
          |
11 | | eqeq2 2421 |
. . . . . . . . . . 11
    
                |
12 | 10, 11 | mpbird 224 |
. . . . . . . . . 10
    
      |
13 | 12 | adantr 452 |
. . . . . . . . 9
      
 
        |
14 | 13 | exlimiv 1641 |
. . . . . . . 8
       
 

        |
15 | 7, 14 | sylbi 188 |
. . . . . . 7
        
 

         |
16 | | cardon 7795 |
. . . . . . 7
     |
17 | 15, 16 | syl6eqelr 2501 |
. . . . . 6
        
 

     |
18 | 17 | ssriv 3320 |
. . . . 5
       
 

    |
19 | | onint0 4743 |
. . . . 5
           
            
 

  
       
 

      |
20 | 18, 19 | ax-mp 8 |
. . . 4
            
             
     |
21 | | 0ex 4307 |
. . . . . 6
 |
22 | | eqeq1 2418 |
. . . . . . . 8

            |
23 | 22 | anbi1d 686 |
. . . . . . 7

      
 
 
       
     |
24 | 23 | exbidv 1633 |
. . . . . 6

       
 

 
       
 
     |
25 | 21, 24 | elab 3050 |
. . . . 5
        
 

            
    |
26 | | onss 4738 |
. . . . . . . . . . 11
   |
27 | | sstr 3324 |
. . . . . . . . . . . 12
 

  |
28 | 27 | ancoms 440 |
. . . . . . . . . . 11
 
   |
29 | 26, 28 | sylan 458 |
. . . . . . . . . 10
  
  |
30 | 29 | 3adant2 976 |
. . . . . . . . 9
     
   |
31 | 30 | 3adant3r 1181 |
. . . . . . . 8
     
 

 
  |
32 | | simp2 958 |
. . . . . . . 8
     
 

        |
33 | | simp3 959 |
. . . . . . . 8
     
 

    
   |
34 | | eqcom 2414 |
. . . . . . . . . . . 12
           |
35 | | vex 2927 |
. . . . . . . . . . . . . 14
 |
36 | | onssnum 7885 |
. . . . . . . . . . . . . 14
     |
37 | 35, 36 | mpan 652 |
. . . . . . . . . . . . 13

  |
38 | | cardnueq0 7815 |
. . . . . . . . . . . . 13
     
   |
39 | 37, 38 | syl 16 |
. . . . . . . . . . . 12

        |
40 | 34, 39 | syl5bb 249 |
. . . . . . . . . . 11

        |
41 | 40 | biimpa 471 |
. . . . . . . . . 10
 
    
  |
42 | | sseq1 3337 |
. . . . . . . . . . . 12


   |
43 | | rexeq 2873 |
. . . . . . . . . . . . 13

 
    |
44 | 43 | ralbidv 2694 |
. . . . . . . . . . . 12

 

 
   |
45 | 42, 44 | anbi12d 692 |
. . . . . . . . . . 11

 
 

  
    |
46 | 45 | biimpa 471 |
. . . . . . . . . 10
  
 
  
 
   |
47 | 41, 46 | sylan 458 |
. . . . . . . . 9
        
 
  
 
   |
48 | | rex0 3609 |
. . . . . . . . . . . . . 14

 |
49 | 48 | rgenw 2741 |
. . . . . . . . . . . . 13

  |
50 | | r19.2z 3685 |
. . . . . . . . . . . . 13
  
  
   |
51 | 49, 50 | mpan2 653 |
. . . . . . . . . . . 12


   |
52 | | rexnal 2685 |
. . . . . . . . . . . 12
    
  |
53 | 51, 52 | sylib 189 |
. . . . . . . . . . 11


   |
54 | 53 | necon4ai 2634 |
. . . . . . . . . 10
 

  |
55 | 54 | adantl 453 |
. . . . . . . . 9
  

   |
56 | 47, 55 | syl 16 |
. . . . . . . 8
        
 
 
  |
57 | 31, 32, 33, 56 | syl21anc 1183 |
. . . . . . 7
     
 

 
  |
58 | 57 | 3expib 1156 |
. . . . . 6
       
 
 
   |
59 | 58 | exlimdv 1643 |
. . . . 5
           
 
   |
60 | 25, 59 | syl5bi 209 |
. . . 4
         
 

      |
61 | 20, 60 | syl5bi 209 |
. . 3
          
 

  
   |
62 | 2, 61 | sylbid 207 |
. 2
         |
63 | | fveq2 5695 |
. . 3

          |
64 | | cf0 8095 |
. . 3
   
 |
65 | 63, 64 | syl6eq 2460 |
. 2

      |
66 | 62, 65 | impbid1 195 |
1
     
   |