Step | Hyp | Ref
| Expression |
1 | | breq2 4420 |
. . . . . 6


   |
2 | 1 | anbi2d 715 |
. . . . 5

 

     |
3 | 2 | exbidv 1779 |
. . . 4

            |
4 | | breq2 4420 |
. . . . . 6
 
   |
5 | 4 | anbi2d 715 |
. . . . 5
  
 
    |
6 | 5 | exbidv 1779 |
. . . 4
             |
7 | | sseq1 3465 |
. . . . . . 7
 
   |
8 | 7 | adantl 472 |
. . . . . 6
 

    |
9 | | breq1 4419 |
. . . . . . 7
 
   |
10 | | breq2 4420 |
. . . . . . 7
 
   |
11 | 9, 10 | sylan9bbr 712 |
. . . . . 6
 


   |
12 | 8, 11 | anbi12d 722 |
. . . . 5
 

 

     |
13 | 12 | cbvexdva 2136 |
. . . 4
    

  
    |
14 | | 0ss 3775 |
. . . . . 6
 |
15 | | 0ex 4549 |
. . . . . . 7
 |
16 | 15 | enref 7628 |
. . . . . 6
 |
17 | | sseq1 3465 |
. . . . . . . 8


   |
18 | | breq1 4419 |
. . . . . . . 8


   |
19 | 17, 18 | anbi12d 722 |
. . . . . . 7

 


    |
20 | 15, 19 | spcev 3153 |
. . . . . 6
         |
21 | 14, 16, 20 | mp2an 683 |
. . . . 5
  
  |
22 | 21 | a1i 11 |
. . . 4
       |
23 | | ssdif0 3835 |
. . . . . . . . . . . . 13

    |
24 | | eqss 3459 |
. . . . . . . . . . . . . . 15

    |
25 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . 19
 
   |
26 | 25 | biimpa 491 |
. . . . . . . . . . . . . . . . . 18
     |
27 | | rspe 2857 |
. . . . . . . . . . . . . . . . . 18
   
  |
28 | 26, 27 | sylan2 481 |
. . . . . . . . . . . . . . . . 17
  
 
   |
29 | | isfi 7619 |
. . . . . . . . . . . . . . . . 17

   |
30 | 28, 29 | sylibr 217 |
. . . . . . . . . . . . . . . 16
  
 
  |
31 | 30 | expcom 441 |
. . . . . . . . . . . . . . 15
       |
32 | 24, 31 | sylanbr 480 |
. . . . . . . . . . . . . 14
  
 

   |
33 | 32 | ex 440 |
. . . . . . . . . . . . 13
 
       |
34 | 23, 33 | sylan2br 483 |
. . . . . . . . . . . 12
 

        |
35 | 34 | expcom 441 |
. . . . . . . . . . 11
  
 
      |
36 | 35 | 3impd 1231 |
. . . . . . . . . 10
  
 
    |
37 | 36 | com12 32 |
. . . . . . . . 9
 
       |
38 | 37 | con3d 140 |
. . . . . . . 8
 
 
     |
39 | | bren 7604 |
. . . . . . . . . . 11

       |
40 | | neq0 3754 |
. . . . . . . . . . . . . . 15
  
     |
41 | | eldifi 3567 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
42 | 41 | snssd 4130 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
43 | | unss 3620 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         |
44 | 43 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
      |
45 | 42, 44 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
46 | 45 | ad2ant2r 758 |
. . . . . . . . . . . . . . . . . . 19
          
        |
47 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
48 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
49 | 47, 48 | f1osn 5875 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
50 | 49 | jctr 549 |
. . . . . . . . . . . . . . . . . . . . . 22
    
    
                |
51 | | eldifn 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
  |
52 | | disjsn 4044 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
  |
53 | 51, 52 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     |
54 | | nnord 6727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
55 | | orddisj 5480 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
57 | 53, 56 | anim12i 574 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     

      |
58 | | f1oun 5856 |
. . . . . . . . . . . . . . . . . . . . . 22
                          
                          |
59 | 50, 57, 58 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . 21
                                |
60 | | df-suc 5448 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
61 | | f1oeq3 5830 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                                      |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
                                     |
63 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
64 | | snex 4655 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      |
65 | 63, 64 | unex 6616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        |
66 | | f1oeq1 5828 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
                  |
67 | 65, 66 | spcev 3153 |
. . . . . . . . . . . . . . . . . . . . . . 23
               
           |
68 | | bren 7604 |
. . . . . . . . . . . . . . . . . . . . . . 23
                |
69 | 67, 68 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . 22
               
   
  |
70 | 62, 69 | sylbir 218 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
71 | 59, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                 |
72 | 71 | adantll 725 |
. . . . . . . . . . . . . . . . . . 19
          
        |
73 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . 21
 |
74 | | snex 4655 |
. . . . . . . . . . . . . . . . . . . . 21
   |
75 | 73, 74 | unex 6616 |
. . . . . . . . . . . . . . . . . . . 20
     |
76 | | sseq1 3465 |
. . . . . . . . . . . . . . . . . . . . 21
             |
77 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . . 21
         
   |
78 | 76, 77 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . 20
       
             |
79 | 75, 78 | spcev 3153 |
. . . . . . . . . . . . . . . . . . 19
         
       |
80 | 46, 72, 79 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
          
    
   |
81 | 80 | expcom 441 |
. . . . . . . . . . . . . . . . 17
   
       
  
    |
82 | 81 | ex 440 |
. . . . . . . . . . . . . . . 16
                   |
83 | 82 | exlimiv 1787 |
. . . . . . . . . . . . . . 15
              
     |
84 | 40, 83 | sylbi 200 |
. . . . . . . . . . . . . 14
                   |
85 | 84 | com13 83 |
. . . . . . . . . . . . 13
 
                 |
86 | 85 | expcom 441 |
. . . . . . . . . . . 12
    
              |
87 | 86 | exlimiv 1787 |
. . . . . . . . . . 11
                    |
88 | 39, 87 | sylbi 200 |
. . . . . . . . . 10
 
             |
89 | 88 | com12 32 |
. . . . . . . . 9
 
             |
90 | 89 | 3imp 1208 |
. . . . . . . 8
 
      
    |
91 | 38, 90 | syld 45 |
. . . . . . 7
 
 
       |
92 | 91 | 3expia 1217 |
. . . . . 6
 
           |
93 | 92 | exlimiv 1787 |
. . . . 5
    


  
     |
94 | 93 | com3l 84 |
. . . 4
 
   
         |
95 | 3, 6, 13, 22, 94 | finds2 6748 |
. . 3
 
       |
96 | 95 | com12 32 |
. 2
         |
97 | 96 | ralrimiv 2812 |
1
        |