Step | Hyp | Ref
| Expression |
1 | | df-qs 5951 |
. . 3
    
   ![]](rbrack.gif)   |
2 | | elimapw1 4944 |
. . . . 5
 ∼  Ins2 S Ins3 SI
   1c  1      
 ∼  Ins2 S Ins3 SI    1c  |
3 | | elima1c 4947 |
. . . . . . . . . 10
       Ins2 S Ins3 SI    1c             Ins2 S Ins3 SI     |
4 | | elsymdif 3223 |
. . . . . . . . . . . 12
           Ins2 S Ins3 SI       
   
  Ins2
S    
   
  Ins3
SI     |
5 | | snex 4111 |
. . . . . . . . . . . . . . . 16
 
 |
6 | 5 | otelins2 5791 |
. . . . . . . . . . . . . . 15
           Ins2 S    
 S  |
7 | | vex 2862 |
. . . . . . . . . . . . . . . 16
 |
8 | | vex 2862 |
. . . . . . . . . . . . . . . 16
 |
9 | 7, 8 | opelssetsn 4760 |
. . . . . . . . . . . . . . 15
      S   |
10 | 6, 9 | bitri 240 |
. . . . . . . . . . . . . 14
           Ins2 S   |
11 | 8 | otelins3 5792 |
. . . . . . . . . . . . . . 15
           Ins3 SI         SI    |
12 | | df-br 4640 |
. . . . . . . . . . . . . . . . 17
          |
13 | | brcnv 4892 |
. . . . . . . . . . . . . . . . 17
        |
14 | 12, 13 | bitr3i 242 |
. . . . . . . . . . . . . . . 16
  
      |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
 |
16 | 7, 15 | opsnelsi 5774 |
. . . . . . . . . . . . . . . 16
        SI
       |
17 | | elec 5964 |
. . . . . . . . . . . . . . . 16
   ![]](rbrack.gif)     |
18 | 14, 16, 17 | 3bitr4i 268 |
. . . . . . . . . . . . . . 15
        SI
   ![]](rbrack.gif)   |
19 | 11, 18 | bitri 240 |
. . . . . . . . . . . . . 14
           Ins3 SI 
  ![]](rbrack.gif)   |
20 | 10, 19 | bibi12i 306 |
. . . . . . . . . . . . 13
            Ins2 S    
   
  Ins3
SI   
  ![]](rbrack.gif)    |
21 | 20 | notbii 287 |
. . . . . . . . . . . 12
     
   
  Ins2
S    
   
  Ins3
SI      ![]](rbrack.gif)    |
22 | 4, 21 | bitri 240 |
. . . . . . . . . . 11
           Ins2 S Ins3 SI      ![]](rbrack.gif)    |
23 | 22 | exbii 1582 |
. . . . . . . . . 10
             Ins2 S
Ins3 SI    
  ![]](rbrack.gif)    |
24 | 3, 23 | bitri 240 |
. . . . . . . . 9
       Ins2 S Ins3 SI    1c  
  ![]](rbrack.gif)    |
25 | 24 | notbii 287 |
. . . . . . . 8
       Ins2 S Ins3 SI
   1c  
  ![]](rbrack.gif)    |
26 | 5, 8 | opex 4588 |
. . . . . . . . 9
   
  |
27 | 26 | elcompl 3225 |
. . . . . . . 8
      ∼  Ins2 S Ins3 SI    1c    
  Ins2 S Ins3 SI    1c  |
28 | | alex 1572 |
. . . . . . . 8
   
  ![]](rbrack.gif)      ![]](rbrack.gif)    |
29 | 25, 27, 28 | 3bitr4i 268 |
. . . . . . 7
      ∼  Ins2 S Ins3 SI    1c      ![]](rbrack.gif)    |
30 | | dfcleq 2347 |
. . . . . . 7
   ![]](rbrack.gif)      ![]](rbrack.gif)    |
31 | 29, 30 | bitr4i 243 |
. . . . . 6
      ∼  Ins2 S Ins3 SI    1c   ![]](rbrack.gif)   |
32 | 31 | rexbii 2639 |
. . . . 5
 
   
 ∼  Ins2 S Ins3 SI    1c    ![]](rbrack.gif)   |
33 | 2, 32 | bitri 240 |
. . . 4
 ∼  Ins2 S Ins3 SI
   1c  1     ![]](rbrack.gif)   |
34 | 33 | abbi2i 2464 |
. . 3
∼  Ins2 S
Ins3 SI    1c  1   
  ![]](rbrack.gif)   |
35 | 1, 34 | eqtr4i 2376 |
. 2
    ∼ 
Ins2 S Ins3 SI    1c  1   |
36 | | ssetex 4744 |
. . . . . . 7
S  |
37 | 36 | ins2ex 5797 |
. . . . . 6
Ins2 S  |
38 | | cnvexg 5101 |
. . . . . . 7
 
  |
39 | | siexg 4752 |
. . . . . . 7
  SI
   |
40 | | ins3exg 5796 |
. . . . . . 7
SI
 Ins3 SI
   |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
 Ins3 SI    |
42 | | symdifexg 4103 |
. . . . . 6
 Ins2 S Ins3 SI   Ins2 S Ins3 SI
    |
43 | 37, 41, 42 | sylancr 644 |
. . . . 5
 Ins2 S Ins3 SI
    |
44 | | 1cex 4142 |
. . . . 5
1c
 |
45 | | imaexg 4746 |
. . . . 5
  Ins2 S
Ins3 SI  
1c
  Ins2 S Ins3 SI    1c   |
46 | 43, 44, 45 | sylancl 643 |
. . . 4
  Ins2 S
Ins3 SI    1c   |
47 | | complexg 4099 |
. . . 4
  Ins2 S
Ins3 SI    1c ∼  Ins2 S
Ins3 SI    1c   |
48 | 46, 47 | syl 15 |
. . 3
 ∼  Ins2 S Ins3 SI
   1c
  |
49 | | pw1exg 4302 |
. . 3
 1   |
50 | | imaexg 4746 |
. . 3
 ∼ 
Ins2 S Ins3 SI    1c 1
 ∼  Ins2 S Ins3 SI    1c  1    |
51 | 48, 49, 50 | syl2an 463 |
. 2
 
 ∼  Ins2 S Ins3 SI    1c  1    |
52 | 35, 51 | syl5eqel 2437 |
1
 
    
  |