Step | Hyp | Ref
| Expression |
1 | | bnj1463.18 |
. . . . . . 7

  |
2 | | elex 3040 |
. . . . . . 7
   |
3 | 1, 2 | syl 17 |
. . . . . 6

  |
4 | | eleq1 2537 |
. . . . . . . 8
 
   |
5 | | fneq2 5675 |
. . . . . . . . 9
 
   |
6 | | raleq 2973 |
. . . . . . . . 9
  
       

           |
7 | 5, 6 | anbi12d 725 |
. . . . . . . 8
                           |
8 | 4, 7 | anbi12d 725 |
. . . . . . 7
                 
             |
9 | | bnj1463.1 |
. . . . . . . . . . . 12
 
         |
10 | 9 | bnj1317 29705 |
. . . . . . . . . . 11
 
  |
11 | 10 | nfcii 2603 |
. . . . . . . . . 10
   |
12 | 11 | nfel2 2628 |
. . . . . . . . 9
  |
13 | | bnj1463.2 |
. . . . . . . . . . . . 13
           |
14 | | bnj1463.3 |
. . . . . . . . . . . . 13
 
             |
15 | | bnj1463.4 |
. . . . . . . . . . . . 13
 
            |
16 | | bnj1463.5 |
. . . . . . . . . . . . 13
     |
17 | | bnj1463.6 |
. . . . . . . . . . . . 13
 
   |
18 | | bnj1463.7 |
. . . . . . . . . . . . 13
  
     |
19 | | bnj1463.8 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)   |
20 | | bnj1463.9 |
. . . . . . . . . . . . 13
 
       |
21 | | bnj1463.10 |
. . . . . . . . . . . . 13
  |
22 | | bnj1463.11 |
. . . . . . . . . . . . 13
           |
23 | | bnj1463.12 |
. . . . . . . . . . . . 13
            |
24 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | bnj1467 29935 |
. . . . . . . . . . . 12
 
  |
25 | 24 | nfcii 2603 |
. . . . . . . . . . 11
   |
26 | | nfcv 2612 |
. . . . . . . . . . 11
   |
27 | 25, 26 | nffn 5682 |
. . . . . . . . . 10
  |
28 | | bnj1463.13 |
. . . . . . . . . . . . 13
           |
29 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 28 | bnj1446 29926 |
. . . . . . . . . . . 12
                     |
30 | 29 | nfi 1682 |
. . . . . . . . . . 11
           |
31 | 26, 30 | nfral 2789 |
. . . . . . . . . 10
            |
32 | 27, 31 | nfan 2031 |
. . . . . . . . 9
              |
33 | 12, 32 | nfan 2031 |
. . . . . . . 8
                |
34 | 33 | nfri 1972 |
. . . . . . 7
  
              
             |
35 | | bnj1463.17 |
. . . . . . . 8

  |
36 | | bnj1463.16 |
. . . . . . . 8
            |
37 | 1, 35, 36 | jca32 544 |
. . . . . . 7
                |
38 | 8, 34, 37 | bnj1465 29728 |
. . . . . 6
                    |
39 | 3, 38 | mpdan 681 |
. . . . 5
    
             |
40 | | df-rex 2762 |
. . . . 5
            
                 |
41 | 39, 40 | sylibr 217 |
. . . 4
  
            |
42 | | bnj1463.15 |
. . . . 5

  |
43 | | nfcv 2612 |
. . . . . . . 8
   |
44 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | bnj1466 29934 |
. . . . . . . . . . 11
 
  |
45 | 44 | nfcii 2603 |
. . . . . . . . . 10
   |
46 | | nfcv 2612 |
. . . . . . . . . 10
   |
47 | 45, 46 | nffn 5682 |
. . . . . . . . 9
  |
48 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 28 | bnj1448 29928 |
. . . . . . . . . . 11
                     |
49 | 48 | nfi 1682 |
. . . . . . . . . 10
           |
50 | 46, 49 | nfral 2789 |
. . . . . . . . 9
            |
51 | 47, 50 | nfan 2031 |
. . . . . . . 8
              |
52 | 43, 51 | nfrex 2848 |
. . . . . . 7
   
           |
53 | 52 | nfri 1972 |
. . . . . 6
                             |
54 | 25 | nfeq2 2627 |
. . . . . . 7
  |
55 | | fneq1 5674 |
. . . . . . . 8
 
   |
56 | | fveq1 5878 |
. . . . . . . . . 10
           |
57 | | reseq1 5105 |
. . . . . . . . . . . . 13
                 |
58 | 57 | opeq2d 4165 |
. . . . . . . . . . . 12
             
         |
59 | 58, 28 | syl6eqr 2523 |
. . . . . . . . . . 11
             |
60 | 59 | fveq2d 5883 |
. . . . . . . . . 10
                     |
61 | 56, 60 | eqeq12d 2486 |
. . . . . . . . 9
           
                   |
62 | 61 | ralbidv 2829 |
. . . . . . . 8
  
         
                    |
63 | 55, 62 | anbi12d 725 |
. . . . . . 7
             
                       |
64 | 54, 63 | rexbid 2891 |
. . . . . 6
  
           
          
             |
65 | 53, 64, 44 | bnj1468 29729 |
. . . . 5
  
 ![]. ].](_drbrack.gif)             
          
             |
66 | 42, 65 | syl 17 |
. . . 4
    ![]. ].](_drbrack.gif)   
                  



            |
67 | 41, 66 | mpbird 240 |
. . 3
   ![]. ].](_drbrack.gif)             
           |
68 | | fveq2 5879 |
. . . . . . . 8
           |
69 | | id 22 |
. . . . . . . . . . 11
   |
70 | | bnj602 29798 |
. . . . . . . . . . . 12
             |
71 | 70 | reseq2d 5111 |
. . . . . . . . . . 11
                 |
72 | 69, 71 | opeq12d 4166 |
. . . . . . . . . 10
             
         |
73 | 13, 72 | syl5eq 2517 |
. . . . . . . . 9
   
         |
74 | 73 | fveq2d 5883 |
. . . . . . . 8
                     |
75 | 68, 74 | eqeq12d 2486 |
. . . . . . 7
         
                     |
76 | 75 | cbvralv 3005 |
. . . . . 6
 
       

                    |
77 | 76 | anbi2i 708 |
. . . . 5
           


                     |
78 | 77 | rexbii 2881 |
. . . 4
            



                     |
79 | 78 | sbcbii 3311 |
. . 3
   ![]. ].](_drbrack.gif) 
          
  ![]. ].](_drbrack.gif)   
                     |
80 | 67, 79 | sylibr 217 |
. 2
   ![]. ].](_drbrack.gif)               |
81 | 14 | bnj1454 29725 |
. . 3
 
  ![]. ].](_drbrack.gif)   
            |
82 | 42, 81 | syl 17 |
. 2
    ![]. ].](_drbrack.gif) 
              |
83 | 80, 82 | mpbird 240 |
1

  |