Step | Hyp | Ref
| Expression |
1 | | df-succf 30688 |
. . 3
Succ Cup Singleton  |
2 | 1 | breqi 4424 |
. 2
 Succ  Cup Singleton    |
3 | | brsuccf.1 |
. . 3
 |
4 | | brsuccf.2 |
. . 3
 |
5 | 3, 4 | brco 5027 |
. 2
  Cup Singleton 
    Singleton Cup   |
6 | | opex 4681 |
. . . . 5
      |
7 | | breq1 4421 |
. . . . 5
     
 Cup      Cup   |
8 | 6, 7 | ceqsexv 3096 |
. . . 4
        
Cup      Cup  |
9 | | snex 4658 |
. . . . 5
 
 |
10 | 3, 9, 4 | brcup 30756 |
. . . 4
  
   Cup

     |
11 | 8, 10 | bitri 257 |
. . 3
        
Cup

     |
12 | 3 | brtxp2 30698 |
. . . . . 6
  Singleton        
Singleton   |
13 | 12 | anbi1i 706 |
. . . . 5
   Singleton Cup         
Singleton Cup   |
14 | | 3anass 995 |
. . . . . . . . 9
    
Singleton      Singleton    |
15 | 14 | anbi1i 706 |
. . . . . . . 8
     
Singleton
Cup       Singleton  Cup   |
16 | | an32 812 |
. . . . . . . 8
      
Singleton  Cup
     Cup 
Singleton    |
17 | | vex 3060 |
. . . . . . . . . . . . 13
 |
18 | 17 | ideq 5009 |
. . . . . . . . . . . 12

  |
19 | | eqcom 2469 |
. . . . . . . . . . . 12

  |
20 | 18, 19 | bitri 257 |
. . . . . . . . . . 11

  |
21 | | vex 3060 |
. . . . . . . . . . . 12
 |
22 | 3, 21 | brsingle 30734 |
. . . . . . . . . . 11
 Singleton     |
23 | 20, 22 | anbi12i 708 |
. . . . . . . . . 10
  Singleton

     |
24 | 23 | anbi1i 706 |
. . . . . . . . 9
   Singleton 
   Cup 
 
       Cup    |
25 | | ancom 456 |
. . . . . . . . 9
      Cup 
Singleton 
 
Singleton     Cup    |
26 | | df-3an 993 |
. . . . . . . . 9
 
      Cup           Cup    |
27 | 24, 25, 26 | 3bitr4i 285 |
. . . . . . . 8
      Cup 
Singleton 

  
   Cup    |
28 | 15, 16, 27 | 3bitri 279 |
. . . . . . 7
     
Singleton
Cup    
   Cup    |
29 | 28 | 2exbii 1730 |
. . . . . 6
         
Singleton
Cup       
    Cup    |
30 | | 19.41vv 1842 |
. . . . . 6
         
Singleton
Cup         
Singleton Cup   |
31 | | opeq1 4180 |
. . . . . . . . 9
         |
32 | 31 | eqeq2d 2472 |
. . . . . . . 8
    
      |
33 | 32 | anbi1d 716 |
. . . . . . 7
      Cup
    Cup    |
34 | | opeq2 4181 |
. . . . . . . . 9
             |
35 | 34 | eqeq2d 2472 |
. . . . . . . 8
      
        |
36 | 35 | anbi1d 716 |
. . . . . . 7
        Cup
     
Cup    |
37 | 3, 9, 33, 36 | ceqsex2v 3099 |
. . . . . 6
     
      Cup        Cup   |
38 | 29, 30, 37 | 3bitr3i 283 |
. . . . 5
         
Singleton
Cup      
Cup   |
39 | 13, 38 | bitri 257 |
. . . 4
   Singleton Cup      
Cup   |
40 | 39 | exbii 1729 |
. . 3
    
Singleton Cup
        Cup   |
41 | | df-suc 5452 |
. . . 4
     |
42 | 41 | eqeq2i 2474 |
. . 3


     |
43 | 11, 40, 42 | 3bitr4i 285 |
. 2
    
Singleton Cup
  |
44 | 2, 5, 43 | 3bitri 279 |
1
 Succ
  |