Step | Hyp | Ref
| Expression |
1 | | df-ref 5901 |
. . 3
Ref     
    |
2 | | vex 2863 |
. . . . . . 7
 |
3 | | vex 2863 |
. . . . . . 7
 |
4 | 2, 3 | opex 4589 |
. . . . . 6
    |
5 | 4 | elcompl 3226 |
. . . . 5
  
 ∼  ∼  SI   S  1c
S  1c     ∼  SI
 
S  1c
S  1c  |
6 | | elima1c 4948 |
. . . . . . . 8
  
  ∼  SI   S  1c
S  1c        
 
∼  SI   S  1c
S   |
7 | | oteltxp 5783 |
. . . . . . . . . 10
      
 
∼  SI   S  1c
S     
 ∼  SI   S  1c    
 S   |
8 | | snex 4112 |
. . . . . . . . . . . . . 14
 
 |
9 | 8, 2 | opex 4589 |
. . . . . . . . . . . . 13
   
  |
10 | 9 | elcompl 3226 |
. . . . . . . . . . . 12
      ∼  SI
 
S  1c    
  SI   S  1c  |
11 | | elima1c 4948 |
. . . . . . . . . . . . . 14
       SI
 
S  1c             SI
 
S   |
12 | | oteltxp 5783 |
. . . . . . . . . . . . . . . 16
           SI
 
S     
   SI      
 S   |
13 | | vex 2863 |
. . . . . . . . . . . . . . . . . . 19
 |
14 | | vex 2863 |
. . . . . . . . . . . . . . . . . . 19
 |
15 | 13, 14 | opsnelsi 5775 |
. . . . . . . . . . . . . . . . . 18
        SI
         |
16 | | elin 3220 |
. . . . . . . . . . . . . . . . . . 19
  
        
    |
17 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . 20
  
     |
18 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . 20
  
     |
19 | 17, 18 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . 19
         
       |
20 | 14, 14 | op1st2nd 5791 |
. . . . . . . . . . . . . . . . . . 19
            |
21 | 16, 19, 20 | 3bitr2i 264 |
. . . . . . . . . . . . . . . . . 18
  
        |
22 | 15, 21 | bitri 240 |
. . . . . . . . . . . . . . . . 17
        SI
   
   |
23 | 13, 2 | opelssetsn 4761 |
. . . . . . . . . . . . . . . . 17
      S   |
24 | 22, 23 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
         SI        S   
    |
25 | 12, 24 | bitri 240 |
. . . . . . . . . . . . . . 15
           SI
 
S        |
26 | 25 | exbii 1582 |
. . . . . . . . . . . . . 14
             SI   S   
 
    |
27 | 11, 26 | bitri 240 |
. . . . . . . . . . . . 13
       SI
 
S  1c          |
28 | | df-br 4641 |
. . . . . . . . . . . . . 14
        |
29 | | df-clel 2349 |
. . . . . . . . . . . . . 14
  

  
 
    |
30 | 28, 29 | bitri 240 |
. . . . . . . . . . . . 13
     
 
    |
31 | 27, 30 | bitr4i 243 |
. . . . . . . . . . . 12
       SI
 
S  1c     |
32 | 10, 31 | xchbinx 301 |
. . . . . . . . . . 11
      ∼  SI
 
S  1c     |
33 | 14, 3 | opelssetsn 4761 |
. . . . . . . . . . 11
      S   |
34 | 32, 33 | anbi12ci 679 |
. . . . . . . . . 10
       ∼
 SI   S  1c    
 S       |
35 | 7, 34 | bitri 240 |
. . . . . . . . 9
      
 
∼  SI   S  1c
S       |
36 | 35 | exbii 1582 |
. . . . . . . 8
           ∼  SI   S  1c S         |
37 | 6, 36 | bitri 240 |
. . . . . . 7
  
  ∼  SI   S  1c
S  1c         |
38 | | df-rex 2621 |
. . . . . . 7
 
    
     |
39 | | rexnal 2626 |
. . . . . . 7
 
  
    |
40 | 37, 38, 39 | 3bitr2i 264 |
. . . . . 6
  
  ∼  SI   S  1c
S  1c 
    |
41 | 40 | con2bii 322 |
. . . . 5
 
 
    ∼  SI
 
S  1c
S  1c  |
42 | 5, 41 | bitr4i 243 |
. . . 4
  
 ∼  ∼  SI   S  1c
S  1c      |
43 | 42 | opabbi2i 4867 |
. . 3
∼  ∼  SI   S  1c S  1c     
    |
44 | 1, 43 | eqtr4i 2376 |
. 2
Ref ∼  ∼  SI   S  1c S  1c |
45 | | 1stex 4740 |
. . . . . . . . . 10
 |
46 | | 2ndex 5113 |
. . . . . . . . . 10
 |
47 | 45, 46 | inex 4106 |
. . . . . . . . 9
   |
48 | 47 | siex 4754 |
. . . . . . . 8
SI  
 |
49 | | ssetex 4745 |
. . . . . . . 8
S  |
50 | 48, 49 | txpex 5786 |
. . . . . . 7
SI
 
S  |
51 | | 1cex 4143 |
. . . . . . 7
1c
 |
52 | 50, 51 | imaex 4748 |
. . . . . 6
 SI   S  1c  |
53 | 52 | complex 4105 |
. . . . 5
∼  SI   S  1c  |
54 | 53, 49 | txpex 5786 |
. . . 4
∼  SI   S  1c S  |
55 | 54, 51 | imaex 4748 |
. . 3
 ∼  SI   S  1c S  1c  |
56 | 55 | complex 4105 |
. 2
∼  ∼  SI   S  1c S  1c  |
57 | 44, 56 | eqeltri 2423 |
1
Ref  |