Step | Hyp | Ref
| Expression |
1 | | enfii 6867 |
. . . 4
  
  |
2 | 1 | 3adant2 1016 |
. . 3
     |
3 | | sseq1 3178 |
. . . . . . 7


   |
4 | | breq1 4003 |
. . . . . . 7


   |
5 | 3, 4 | anbi12d 473 |
. . . . . 6

 


    |
6 | | eqeq1 2184 |
. . . . . 6


   |
7 | 5, 6 | imbi12d 234 |
. . . . 5

  
    
    |
8 | 7 | albidv 1824 |
. . . 4

      
   
     |
9 | | sseq1 3178 |
. . . . . . 7
 
   |
10 | | breq1 4003 |
. . . . . . 7
 
   |
11 | 9, 10 | anbi12d 473 |
. . . . . 6
  
 
    |
12 | | eqeq1 2184 |
. . . . . 6
 
   |
13 | 11, 12 | imbi12d 234 |
. . . . 5
    

 
     |
14 | 13 | albidv 1824 |
. . . 4
       
    
    |
15 | | sseq1 3178 |
. . . . . . 7
             |
16 | | breq1 4003 |
. . . . . . 7
             |
17 | 15, 16 | anbi12d 473 |
. . . . . 6
       
             |
18 | | eqeq1 2184 |
. . . . . 6
             |
19 | 17, 18 | imbi12d 234 |
. . . . 5
       

           
        |
20 | 19 | albidv 1824 |
. . . 4
          

       
             |
21 | | sseq1 3178 |
. . . . . . 7
 
   |
22 | | breq1 4003 |
. . . . . . 7
 
   |
23 | 21, 22 | anbi12d 473 |
. . . . . 6
  
 
    |
24 | | eqeq1 2184 |
. . . . . 6
 
   |
25 | 23, 24 | imbi12d 234 |
. . . . 5
    

       |
26 | 25 | albidv 1824 |
. . . 4
       
    
    |
27 | | ensym 6774 |
. . . . . . . 8

  |
28 | | en0 6788 |
. . . . . . . 8

  |
29 | 27, 28 | sylib 122 |
. . . . . . 7

  |
30 | 29 | eqcomd 2183 |
. . . . . 6

  |
31 | 30 | adantl 277 |
. . . . 5
  
  |
32 | 31 | ax-gen 1449 |
. . . 4
   
   |
33 | | sseq2 3179 |
. . . . . . . 8
 
   |
34 | | breq2 4004 |
. . . . . . . 8
 
   |
35 | 33, 34 | anbi12d 473 |
. . . . . . 7
  
 
    |
36 | | eqeq2 2187 |
. . . . . . 7
 
   |
37 | 35, 36 | imbi12d 234 |
. . . . . 6
    

 
     |
38 | 37 | cbvalv 1917 |
. . . . 5
      
    
   |
39 | | simplr 528 |
. . . . . . . . . . 11
   
            
              |
40 | | difun2 3502 |
. . . . . . . . . . . . . 14
             |
41 | | difsn 3728 |
. . . . . . . . . . . . . . 15
       |
42 | 41 | ad3antlr 493 |
. . . . . . . . . . . . . 14
   
            
            |
43 | 40, 42 | eqtrid 2222 |
. . . . . . . . . . . . 13
   
            
                |
44 | | simprl 529 |
. . . . . . . . . . . . . 14
   
            
            |
45 | 44 | ssdifd 3271 |
. . . . . . . . . . . . 13
   
            
             
      |
46 | 43, 45 | eqsstrrd 3192 |
. . . . . . . . . . . 12
   
            
     
      |
47 | | simplll 533 |
. . . . . . . . . . . . . . 15
   
            
        |
48 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
49 | 48 | a1i 9 |
. . . . . . . . . . . . . . 15
   
            
        |
50 | | simpllr 534 |
. . . . . . . . . . . . . . 15
   
            
     
  |
51 | | unsnfi 6911 |
. . . . . . . . . . . . . . 15
 
       |
52 | 47, 49, 50, 51 | syl3anc 1238 |
. . . . . . . . . . . . . 14
   
            
            |
53 | | simprr 531 |
. . . . . . . . . . . . . 14
   
            
            |
54 | | vsnid 3623 |
. . . . . . . . . . . . . . . 16
   |
55 | | elun2 3303 |
. . . . . . . . . . . . . . . 16
         |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
57 | 56 | a1i 9 |
. . . . . . . . . . . . . 14
   
            
            |
58 | 44, 57 | sseldd 3156 |
. . . . . . . . . . . . . 14
   
            
        |
59 | 52, 53, 57, 58 | dif1enen 6873 |
. . . . . . . . . . . . 13
   
            
                    |
60 | 43, 59 | eqbrtrrd 4024 |
. . . . . . . . . . . 12
   
            
     
      |
61 | 46, 60 | jca 306 |
. . . . . . . . . . 11
   
            
       
          |
62 | | vex 2740 |
. . . . . . . . . . . . 13
 |
63 | | difexg 4141 |
. . . . . . . . . . . . 13
 
     |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . 12
     |
65 | | sseq2 3179 |
. . . . . . . . . . . . . 14
     
       |
66 | | breq2 4004 |
. . . . . . . . . . . . . 14
             |
67 | 65, 66 | anbi12d 473 |
. . . . . . . . . . . . 13
       
             |
68 | | eqeq2 2187 |
. . . . . . . . . . . . 13
             |
69 | 67, 68 | imbi12d 234 |
. . . . . . . . . . . 12
       
    
                |
70 | 64, 69 | spcv 2831 |
. . . . . . . . . . 11
         
               |
71 | 39, 61, 70 | sylc 62 |
. . . . . . . . . 10
   
            
            |
72 | 71 | uneq1d 3288 |
. . . . . . . . 9
   
            
                    |
73 | 53 | ensymd 6776 |
. . . . . . . . . . 11
   
            
            |
74 | | enfii 6867 |
. . . . . . . . . . 11
     
       |
75 | 52, 73, 74 | syl2anc 411 |
. . . . . . . . . 10
   
            
     
  |
76 | | fidifsnid 6864 |
. . . . . . . . . 10
 
           |
77 | 75, 58, 76 | syl2anc 411 |
. . . . . . . . 9
   
            
                |
78 | 72, 77 | eqtrd 2210 |
. . . . . . . 8
   
            
            |
79 | 78 | ex 115 |
. . . . . . 7
        
       
            |
80 | 79 | alrimiv 1874 |
. . . . . 6
        
                      |
81 | 80 | ex 115 |
. . . . 5
 

                            |
82 | 38, 81 | biimtrid 152 |
. . . 4
 

              
             |
83 | 8, 14, 20, 26, 32, 82 | findcard2s 6883 |
. . 3
     
   |
84 | 2, 83 | syl 14 |
. 2
       
   |
85 | | 3simpc 996 |
. 2
       |
86 | | sseq2 3179 |
. . . . . 6
 
   |
87 | | breq2 4004 |
. . . . . 6
 
   |
88 | 86, 87 | anbi12d 473 |
. . . . 5
  
 
    |
89 | | eqeq2 2187 |
. . . . 5
 
   |
90 | 88, 89 | imbi12d 234 |
. . . 4
    

       |
91 | 90 | spcgv 2824 |
. . 3
         
     |
92 | 91 | 3ad2ant1 1018 |
. 2
           
     |
93 | 84, 85, 92 | mp2d 47 |
1
     |