Step | Hyp | Ref
| Expression |
1 | | xpeq1 4640 |
. . . . 5

  
   |
2 | 1 | eleq1d 2246 |
. . . 4

  
     |
3 | 2 | imbi2d 230 |
. . 3

    

      |
4 | | xpeq1 4640 |
. . . . 5
               |
5 | 4 | eleq1d 2246 |
. . . 4
                 |
6 | 5 | imbi2d 230 |
. . 3
         

 
        |
7 | | xpeq1 4640 |
. . . . 5
       |
8 | 7 | eleq1d 2246 |
. . . 4
   
     |
9 | 8 | imbi2d 230 |
. . 3
             |
10 | | xpeq1 4640 |
. . . . 5
       |
11 | 10 | eleq1d 2246 |
. . . 4
   
     |
12 | 11 | imbi2d 230 |
. . 3
             |
13 | | 0xp 4706 |
. . . . 5
   |
14 | | 0fin 6883 |
. . . . 5
 |
15 | 13, 14 | eqeltri 2250 |
. . . 4
   |
16 | 15 | a1i 9 |
. . 3
     |
17 | | xpeq1 4640 |
. . . . . . . 8

  
   |
18 | 17, 15 | eqeltrdi 2268 |
. . . . . . 7

    |
19 | 18 | a1i13 24 |
. . . . . 6
 
                  |
20 | | sneq 3603 |
. . . . . . . . . . . . . . 15
       |
21 | 20 | difeq2d 3253 |
. . . . . . . . . . . . . 14
 
         |
22 | 21 | xpeq1d 4649 |
. . . . . . . . . . . . 13
               |
23 | 22 | eleq1d 2246 |
. . . . . . . . . . . 12
                 |
24 | 23 | imbi2d 230 |
. . . . . . . . . . 11
         

 
        |
25 | 24 | rspcv 2837 |
. . . . . . . . . 10
  
        
          |
26 | 25 | adantl 277 |
. . . . . . . . 9
   

 

                  |
27 | | pm2.27 40 |
. . . . . . . . . 10
                   |
28 | 27 | ad2antlr 489 |
. . . . . . . . 9
   

 
                |
29 | | vex 2740 |
. . . . . . . . . . . . . . 15
 |
30 | 29 | snex 4185 |
. . . . . . . . . . . . . 14
 
 |
31 | | xpexg 4740 |
. . . . . . . . . . . . . 14
           |
32 | 30, 31 | mpan 424 |
. . . . . . . . . . . . 13
       |
33 | | id 19 |
. . . . . . . . . . . . 13
   |
34 | | 2ndconst 6222 |
. . . . . . . . . . . . . 14
                 |
35 | 29, 34 | mp1i 10 |
. . . . . . . . . . . . 13
                 |
36 | | f1oen2g 6754 |
. . . . . . . . . . . . 13
      
                    |
37 | 32, 33, 35, 36 | syl3anc 1238 |
. . . . . . . . . . . 12
       |
38 | | enfii 6873 |
. . . . . . . . . . . 12
      
      |
39 | 37, 38 | mpdan 421 |
. . . . . . . . . . 11
       |
40 | 39 | ad2antlr 489 |
. . . . . . . . . 10
   

      |
41 | | incom 3327 |
. . . . . . . . . . . . . 14
   
             |
42 | | disjdif 3495 |
. . . . . . . . . . . . . 14
   
     |
43 | 41, 42 | eqtr3i 2200 |
. . . . . . . . . . . . 13
         |
44 | | xpdisj1 5053 |
. . . . . . . . . . . . 13
        
              |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . . 12
             |
46 | | unfidisj 6920 |
. . . . . . . . . . . 12
       
                               |
47 | 45, 46 | mp3an3 1326 |
. . . . . . . . . . 11
       
                   |
48 | | xpundir 4683 |
. . . . . . . . . . . . 13
                       |
49 | | fidifsnid 6870 |
. . . . . . . . . . . . . . 15
 
           |
50 | 49 | adantlr 477 |
. . . . . . . . . . . . . 14
   

 
        |
51 | 50 | xpeq1d 4649 |
. . . . . . . . . . . . 13
   

              |
52 | 48, 51 | eqtr3id 2224 |
. . . . . . . . . . . 12
   

                |
53 | 52 | eleq1d 2246 |
. . . . . . . . . . 11
   

                  |
54 | 47, 53 | imbitrid 154 |
. . . . . . . . . 10
   

       
          |
55 | 40, 54 | mpan2d 428 |
. . . . . . . . 9
   

            |
56 | 26, 28, 55 | 3syld 57 |
. . . . . . . 8
   

 

            |
57 | 56 | ex 115 |
. . . . . . 7
 
   

 
           |
58 | 57 | exlimdv 1819 |
. . . . . 6
 
    
              |
59 | | fin0or 6885 |
. . . . . . 7
  
   |
60 | 59 | adantr 276 |
. . . . . 6
 
      |
61 | 19, 58, 60 | mpjaod 718 |
. . . . 5
 
                |
62 | 61 | ex 115 |
. . . 4
 
 
              |
63 | 62 | com23 78 |
. . 3
  
        
      |
64 | 3, 6, 9, 12, 16, 63 | findcard 6887 |
. 2
 
     |
65 | 64 | imp 124 |
1
 
     |