Step | Hyp | Ref
| Expression |
1 | | indpi.4 |
. 2
     |
2 | | elni 7306 |
. . 3

    |
3 | | eqid 2177 |
. . . . . . . . . 10
 |
4 | 3 | orci 731 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)   |
5 | | nfv 1528 |
. . . . . . . . . . 11
   |
6 | | nfsbc1v 2981 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)  |
7 | 5, 6 | nfor 1574 |
. . . . . . . . . 10
     ![]. ].](_drbrack.gif)   |
8 | | 0ex 4130 |
. . . . . . . . . 10
 |
9 | | eqeq1 2184 |
. . . . . . . . . . 11


   |
10 | | sbceq1a 2972 |
. . . . . . . . . . 11

   ![]. ].](_drbrack.gif)    |
11 | 9, 10 | orbi12d 793 |
. . . . . . . . . 10

   
  ![]. ].](_drbrack.gif)     |
12 | 7, 8, 11 | elabf 2880 |
. . . . . . . . 9
    
   ![]. ].](_drbrack.gif)    |
13 | 4, 12 | mpbir 146 |
. . . . . . . 8
 
   |
14 | | suceq 4402 |
. . . . . . . . . . . . . 14

  |
15 | | df-1o 6416 |
. . . . . . . . . . . . . 14
 |
16 | 14, 15 | eqtr4di 2228 |
. . . . . . . . . . . . 13

  |
17 | | indpi.5 |
. . . . . . . . . . . . . . 15
 |
18 | 17 | olci 732 |
. . . . . . . . . . . . . 14

  |
19 | | 1oex 6424 |
. . . . . . . . . . . . . . 15
 |
20 | | eqeq1 2184 |
. . . . . . . . . . . . . . . 16
 
   |
21 | | indpi.1 |
. . . . . . . . . . . . . . . 16
     |
22 | 20, 21 | orbi12d 793 |
. . . . . . . . . . . . . . 15
   
     |
23 | 19, 22 | elab 2881 |
. . . . . . . . . . . . . 14
    
    |
24 | 18, 23 | mpbir 146 |
. . . . . . . . . . . . 13
 
   |
25 | 16, 24 | eqeltrdi 2268 |
. . . . . . . . . . . 12

      |
26 | 25 | a1d 22 |
. . . . . . . . . . 11

            |
27 | 26 | a1i 9 |
. . . . . . . . . 10
      
 
      |
28 | | indpi.6 |
. . . . . . . . . . . 12
     |
29 | | elni 7306 |
. . . . . . . . . . . . . . . 16

    |
30 | 29 | simprbi 275 |
. . . . . . . . . . . . . . 15
   |
31 | 30 | neneqd 2368 |
. . . . . . . . . . . . . 14

  |
32 | | biorf 744 |
. . . . . . . . . . . . . 14
       |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . . 13
       |
34 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
35 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
 
   |
36 | | indpi.2 |
. . . . . . . . . . . . . . 15
     |
37 | 35, 36 | orbi12d 793 |
. . . . . . . . . . . . . 14
   
     |
38 | 34, 37 | elab 2881 |
. . . . . . . . . . . . 13
    
    |
39 | 33, 38 | bitr4di 198 |
. . . . . . . . . . . 12
         |
40 | | 1pi 7313 |
. . . . . . . . . . . . . . . . . 18
 |
41 | | addclpi 7325 |
. . . . . . . . . . . . . . . . . 18
    
  |
42 | 40, 41 | mpan2 425 |
. . . . . . . . . . . . . . . . 17
     |
43 | | elni 7306 |
. . . . . . . . . . . . . . . . 17
  
        |
44 | 42, 43 | sylib 122 |
. . . . . . . . . . . . . . . 16
   
     |
45 | 44 | simprd 114 |
. . . . . . . . . . . . . . 15
     |
46 | 45 | neneqd 2368 |
. . . . . . . . . . . . . 14
  
  |
47 | | biorf 744 |
. . . . . . . . . . . . . 14
  
        |
48 | 46, 47 | syl 14 |
. . . . . . . . . . . . 13
         |
49 | | eqeq1 2184 |
. . . . . . . . . . . . . . . 16
   
     |
50 | | indpi.3 |
. . . . . . . . . . . . . . . 16
       |
51 | 49, 50 | orbi12d 793 |
. . . . . . . . . . . . . . 15
     
  
    |
52 | 51 | elabg 2883 |
. . . . . . . . . . . . . 14
     
           |
53 | 42, 52 | syl 14 |
. . . . . . . . . . . . 13
   
           |
54 | | addpiord 7314 |
. . . . . . . . . . . . . . . 16
    
    |
55 | 40, 54 | mpan2 425 |
. . . . . . . . . . . . . . 15
       |
56 | | pion 7308 |
. . . . . . . . . . . . . . . 16
   |
57 | | oa1suc 6467 |
. . . . . . . . . . . . . . . 16
     |
58 | 56, 57 | syl 14 |
. . . . . . . . . . . . . . 15
     |
59 | 55, 58 | eqtrd 2210 |
. . . . . . . . . . . . . 14
     |
60 | 59 | eleq1d 2246 |
. . . . . . . . . . . . 13
   
   
       |
61 | 48, 53, 60 | 3bitr2d 216 |
. . . . . . . . . . . 12
   
     |
62 | 28, 39, 61 | 3imtr3d 202 |
. . . . . . . . . . 11
     
 
     |
63 | 62 | a1i 9 |
. . . . . . . . . 10
      
 
      |
64 | | nndceq0 4617 |
. . . . . . . . . . . 12

DECID
  |
65 | | df-dc 835 |
. . . . . . . . . . . 12
DECID     |
66 | 64, 65 | sylib 122 |
. . . . . . . . . . 11
 
   |
67 | | idd 21 |
. . . . . . . . . . . . . . 15
     |
68 | 67 | necon3bd 2390 |
. . . . . . . . . . . . . 14
 
   |
69 | 68 | anc2li 329 |
. . . . . . . . . . . . 13
 
     |
70 | 69, 29 | imbitrrdi 162 |
. . . . . . . . . . . 12
 
   |
71 | 70 | orim2d 788 |
. . . . . . . . . . 11
         |
72 | 66, 71 | mpd 13 |
. . . . . . . . . 10
     |
73 | 27, 63, 72 | mpjaod 718 |
. . . . . . . . 9
     
 
     |
74 | 73 | rgen 2530 |
. . . . . . . 8
     
      |
75 | | peano5 4597 |
. . . . . . . 8
 
         
            |
76 | 13, 74, 75 | mp2an 426 |
. . . . . . 7
     |
77 | 76 | sseli 3151 |
. . . . . 6
       |
78 | | abid 2165 |
. . . . . 6
    
    |
79 | 77, 78 | sylib 122 |
. . . . 5
     |
80 | 79 | adantr 276 |
. . . 4
       |
81 | | df-ne 2348 |
. . . . . 6

  |
82 | | biorf 744 |
. . . . . 6
       |
83 | 81, 82 | sylbi 121 |
. . . . 5

      |
84 | 83 | adantl 277 |
. . . 4
         |
85 | 80, 84 | mpbird 167 |
. . 3
     |
86 | 2, 85 | sylbi 121 |
. 2
   |
87 | 1, 86 | vtoclga 2803 |
1
   |