Step | Hyp | Ref
| Expression |
1 | | elrn2 4897 |
. 2
  
 Ins3           AddC           AddC          Ins3           AddC           AddC    |
2 | | elin 3219 |
. . . 4
  
    Ins3        
  AddC           AddC         Ins3           AddC    
            AddC    |
3 | | vex 2862 |
. . . . . . 7
 |
4 | 3 | otelins3 5792 |
. . . . . 6
  
    Ins3           AddC              AddC   |
5 | | opelcnv 4893 |
. . . . . 6
  
           AddC             AddC   |
6 | | trtxp 5781 |
. . . . . . . . . 10
                          |
7 | | df-br 4640 |
. . . . . . . . . . . 12
       
          |
8 | | elrn2 4897 |
. . . . . . . . . . . 12
  
     
               |
9 | | vex 2862 |
. . . . . . . . . . . . . . 15
 |
10 | 9 | proj1ex 4593 |
. . . . . . . . . . . . . 14
Proj1  |
11 | 10 | eqvinc 2966 |
. . . . . . . . . . . . 13
Proj1
 
    Proj1
      |
12 | | opeq 4619 |
. . . . . . . . . . . . . . 15
Proj1  Proj2   |
13 | 12 | breq1i 4646 |
. . . . . . . . . . . . . 14
      Proj1  Proj2         |
14 | 9 | proj2ex 4594 |
. . . . . . . . . . . . . . 15
Proj2  |
15 | 10, 14 | opbr1st 5501 |
. . . . . . . . . . . . . 14
 Proj1

Proj2     
 Proj1
 
   |
16 | 13, 15 | bitri 240 |
. . . . . . . . . . . . 13
      Proj1      |
17 | | oteltxp 5782 |
. . . . . . . . . . . . . . 15
  
                      |
18 | | opelcnv 4893 |
. . . . . . . . . . . . . . . . 17
  
       |
19 | | df-br 4640 |
. . . . . . . . . . . . . . . . 17
  
     |
20 | 12 | breq1i 4646 |
. . . . . . . . . . . . . . . . . 18
  
Proj1  Proj2      |
21 | 10, 14 | opbr1st 5501 |
. . . . . . . . . . . . . . . . . 18
 Proj1

Proj2    Proj1   |
22 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . 18
Proj1
Proj1   |
23 | 20, 21, 22 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
  
Proj1
  |
24 | 18, 19, 23 | 3bitr2i 264 |
. . . . . . . . . . . . . . . 16
  
  Proj1   |
25 | | elin 3219 |
. . . . . . . . . . . . . . . . 17
  
        
    |
26 | | df-br 4640 |
. . . . . . . . . . . . . . . . . 18
  
     |
27 | | df-br 4640 |
. . . . . . . . . . . . . . . . . 18
  
     |
28 | 26, 27 | anbi12i 678 |
. . . . . . . . . . . . . . . . 17
         
       |
29 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
 |
30 | 29, 29 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . 17
            |
31 | 25, 28, 30 | 3bitr2i 264 |
. . . . . . . . . . . . . . . 16
  
        |
32 | 24, 31 | anbi12i 678 |
. . . . . . . . . . . . . . 15
       
   
 Proj1
 
    |
33 | 17, 32 | bitri 240 |
. . . . . . . . . . . . . 14
  
         
Proj1       |
34 | 33 | exbii 1582 |
. . . . . . . . . . . . 13
      
          Proj1
 
    |
35 | 11, 16, 34 | 3bitr4ri 269 |
. . . . . . . . . . . 12
      
              |
36 | 7, 8, 35 | 3bitri 262 |
. . . . . . . . . . 11
       
   
   |
37 | 36 | anbi1i 676 |
. . . . . . . . . 10
                       |
38 | 29, 29 | opex 4588 |
. . . . . . . . . . 11
    |
39 | | vex 2862 |
. . . . . . . . . . 11
 |
40 | 38, 39 | op1st2nd 5790 |
. . . . . . . . . 10
                  |
41 | 6, 37, 40 | 3bitri 262 |
. . . . . . . . 9
                     |
42 | 41 | rexbii 2639 |
. . . . . . . 8
 
AddC              AddC         |
43 | | elima 4754 |
. . . . . . . 8
  
          AddC  AddC           
   |
44 | | df-br 4640 |
. . . . . . . . 9
  
 AddC
      AddC  |
45 | | risset 2661 |
. . . . . . . . 9
   
   AddC  AddC         |
46 | 44, 45 | bitri 240 |
. . . . . . . 8
  
 AddC
 AddC         |
47 | 42, 43, 46 | 3bitr4i 268 |
. . . . . . 7
  
          AddC    AddC   |
48 | 29, 29 | braddcfn 5826 |
. . . . . . 7
  
 AddC
    |
49 | | eqcom 2355 |
. . . . . . 7
       |
50 | 47, 48, 49 | 3bitri 262 |
. . . . . 6
  
          AddC     |
51 | 4, 5, 50 | 3bitri 262 |
. . . . 5
  
    Ins3           AddC     |
52 | | elima 4754 |
. . . . . . 7
  
       
      AddC  AddC                   |
53 | | trtxp 5781 |
. . . . . . . . 9
    
                             |
54 | | trtxp 5781 |
. . . . . . . . . . 11
    
               |
55 | 54 | anbi2i 675 |
. . . . . . . . . 10
             
                  |
56 | | anass 630 |
. . . . . . . . . 10
                   
    
      |
57 | 39, 29 | op1st2nd 5790 |
. . . . . . . . . . . 12
 Proj1   Proj1    Proj1      |
58 | | brco 4883 |
. . . . . . . . . . . . . 14
    
          |
59 | 12 | breq1i 4646 |
. . . . . . . . . . . . . . . . 17
  
Proj1  Proj2      |
60 | 10, 14 | opbr1st 5501 |
. . . . . . . . . . . . . . . . 17
 Proj1

Proj2    Proj1   |
61 | | eqcom 2355 |
. . . . . . . . . . . . . . . . 17
Proj1
Proj1   |
62 | 59, 60, 61 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
  
Proj1
  |
63 | 62 | anbi1i 676 |
. . . . . . . . . . . . . . 15
        Proj1      |
64 | 63 | exbii 1582 |
. . . . . . . . . . . . . 14
            Proj1      |
65 | | breq1 4642 |
. . . . . . . . . . . . . . 15
 Proj1    Proj1      |
66 | 10, 65 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
   
Proj1    Proj1     |
67 | 58, 64, 66 | 3bitri 262 |
. . . . . . . . . . . . 13
    
Proj1     |
68 | | brco 4883 |
. . . . . . . . . . . . . 14
    
          |
69 | 23 | anbi1i 676 |
. . . . . . . . . . . . . . 15
        Proj1      |
70 | 69 | exbii 1582 |
. . . . . . . . . . . . . 14
            Proj1      |
71 | | breq1 4642 |
. . . . . . . . . . . . . . 15
 Proj1    Proj1      |
72 | 10, 71 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
   
Proj1    Proj1     |
73 | 68, 70, 72 | 3bitri 262 |
. . . . . . . . . . . . 13
    
Proj1     |
74 | 67, 73 | anbi12i 678 |
. . . . . . . . . . . 12
          
Proj1   Proj1      |
75 | 12 | breq1i 4646 |
. . . . . . . . . . . . 13
      Proj1  Proj2         |
76 | 10, 14 | opbr1st 5501 |
. . . . . . . . . . . . 13
 Proj1

Proj2     
 Proj1
 
   |
77 | 75, 76 | bitri 240 |
. . . . . . . . . . . 12
      Proj1      |
78 | 57, 74, 77 | 3bitr4i 268 |
. . . . . . . . . . 11
          
   
   |
79 | 78 | anbi1i 676 |
. . . . . . . . . 10
                          |
80 | 55, 56, 79 | 3bitr2i 264 |
. . . . . . . . 9
             
      
      |
81 | 39, 29 | opex 4588 |
. . . . . . . . . 10
    |
82 | 81, 3 | op1st2nd 5790 |
. . . . . . . . 9
                  |
83 | 53, 80, 82 | 3bitri 262 |
. . . . . . . 8
    
              
     |
84 | 83 | rexbii 2639 |
. . . . . . 7
 
AddC            
     AddC         |
85 | 52, 84 | bitri 240 |
. . . . . 6
  
       
      AddC  AddC         |
86 | | df-br 4640 |
. . . . . . 7
  
 AddC
      AddC  |
87 | | risset 2661 |
. . . . . . 7
   
   AddC  AddC         |
88 | 86, 87 | bitr2i 241 |
. . . . . 6
 
AddC          AddC
  |
89 | 39, 29 | braddcfn 5826 |
. . . . . . 7
  
 AddC
    |
90 | | eqcom 2355 |
. . . . . . 7
       |
91 | 89, 90 | bitri 240 |
. . . . . 6
  
 AddC
    |
92 | 85, 88, 91 | 3bitri 262 |
. . . . 5
  
       
      AddC     |
93 | 51, 92 | anbi12i 678 |
. . . 4
        Ins3        
  AddC  
       
      AddC    
     |
94 | 2, 93 | bitri 240 |
. . 3
  
    Ins3        
  AddC           AddC    
     |
95 | 94 | exbii 1582 |
. 2
      
 
Ins3           AddC           AddC    
 
     |
96 | 29, 29 | addcex 4394 |
. . 3
   |
97 | | addceq1 4383 |
. . . 4
  
    
   |
98 | 97 | eqeq2d 2364 |
. . 3
  

    
    |
99 | 96, 98 | ceqsexv 2894 |
. 2
     
         |
100 | 1, 95, 99 | 3bitri 262 |
1
  
 Ins3           AddC           AddC        |