Step | Hyp | Ref
| Expression |
1 | | nchoicelem10.2 |
. 2
 |
2 | | elrn 4897 |
. . . . 5
       ∼ S  S  S Image      ∼
S  S  S Image       
   |
3 | | trtxp 5782 |
. . . . . . 7
   ∼
S  S  S Image       
   ∼
S     S  S Image      |
4 | | brcnv 4893 |
. . . . . . . . . 10
  ∼ S     ∼ S   |
5 | | df-br 4641 |
. . . . . . . . . 10
   ∼ S      ∼
S  |
6 | | snex 4112 |
. . . . . . . . . . . . 13
 
 |
7 | | vex 2863 |
. . . . . . . . . . . . 13
 |
8 | 6, 7 | opex 4589 |
. . . . . . . . . . . 12
   
  |
9 | 8 | elcompl 3226 |
. . . . . . . . . . 11
      ∼ S      S  |
10 | | vex 2863 |
. . . . . . . . . . . 12
 |
11 | 10, 7 | opelssetsn 4761 |
. . . . . . . . . . 11
      S   |
12 | 9, 11 | xchbinx 301 |
. . . . . . . . . 10
      ∼ S   |
13 | 4, 5, 12 | 3bitri 262 |
. . . . . . . . 9
  ∼ S     |
14 | | brres 4950 |
. . . . . . . . . 10
   S  S Image     S
 S Image    |
15 | | brcnv 4893 |
. . . . . . . . . . . 12
  S S   |
16 | 1, 7 | brsset 4759 |
. . . . . . . . . . . 12
 S   |
17 | 15, 16 | bitri 240 |
. . . . . . . . . . 11
  S
  |
18 | | elfix 5788 |
. . . . . . . . . . . 12
  S
Image  S Image    |
19 | | brco 4884 |
. . . . . . . . . . . . 13
  S Image     Image S    |
20 | | vex 2863 |
. . . . . . . . . . . . . . . 16
 |
21 | 7, 20 | brimage 5794 |
. . . . . . . . . . . . . . 15
 Image
      |
22 | 20, 7 | brsset 4759 |
. . . . . . . . . . . . . . 15
 S   |
23 | 21, 22 | anbi12i 678 |
. . . . . . . . . . . . . 14
  Image S          |
24 | 23 | exbii 1582 |
. . . . . . . . . . . . 13
    Image S 
  
       |
25 | | nchoicelem10.1 |
. . . . . . . . . . . . . . 15
 |
26 | 25, 7 | imaex 4748 |
. . . . . . . . . . . . . 14
     |
27 | | sseq1 3293 |
. . . . . . . . . . . . . 14
    
        |
28 | 26, 27 | ceqsexv 2895 |
. . . . . . . . . . . . 13
       
       |
29 | 19, 24, 28 | 3bitri 262 |
. . . . . . . . . . . 12
  S Image        |
30 | 18, 29 | bitri 240 |
. . . . . . . . . . 11
  S
Image       |
31 | 17, 30 | anbi12i 678 |
. . . . . . . . . 10
   S  S Image  
       |
32 | 14, 31 | bitri 240 |
. . . . . . . . 9
   S  S Image       
   |
33 | 13, 32 | anbi12i 678 |
. . . . . . . 8
   ∼
S     S  S Image     
        |
34 | | ancom 437 |
. . . . . . . 8
              
    |
35 | 33, 34 | bitri 240 |
. . . . . . 7
   ∼
S     S  S Image         
    |
36 | | annim 414 |
. . . . . . 7
       
  
    
   |
37 | 3, 35, 36 | 3bitri 262 |
. . . . . 6
   ∼
S  S  S Image       
      
    |
38 | 37 | exbii 1582 |
. . . . 5
    ∼ S  S
 S Image       
   
        |
39 | | exnal 1574 |
. . . . 5
   
    
        
    |
40 | 2, 38, 39 | 3bitrri 263 |
. . . 4
    
    
    
  ∼ S  S
 S Image     |
41 | 40 | con1bii 321 |
. . 3
       ∼ S  S  S Image           
   |
42 | 6, 1 | opex 4589 |
. . . 4
   
  |
43 | 42 | elcompl 3226 |
. . 3
      ∼
 ∼ S
 S  S Image         ∼ S  S  S Image     |
44 | | df-clos1 5874 |
. . . . 5
Clos1   
          |
45 | 44 | eleq2i 2417 |
. . . 4
 Clos1     
         |
46 | 10 | elintab 3938 |
. . . 4
             
    
   |
47 | 45, 46 | bitri 240 |
. . 3
 Clos1       
    
   |
48 | 41, 43, 47 | 3bitr4i 268 |
. 2
      ∼
 ∼ S
 S  S Image   Clos1      |
49 | 1, 48 | releqel 5808 |
1
  
 ∼  Ins3 S Ins2 ∼  ∼
S  S  S Image     1c
Clos1      |