Proof of Theorem relcoi1
Step | Hyp | Ref
| Expression |
1 | | relfld 4789 |
. . 3

      |
2 | | resundi 4568 |
. . . . 5
        |
3 | | coeq2 4437 |
. . . . 5

   
  

     
      |
4 | | coundi 4765 |
. . . . . . 7
               |
5 | | resco 4768 |
. . . . . . . 8
       |
6 | | coi1 4779 |
. . . . . . . . 9

   |
7 | | reseq1 4549 |
. . . . . . . . . 10
 
 
     |
8 | | resdm 4592 |
. . . . . . . . . . 11

    |
9 | | eqtr 2054 |
. . . . . . . . . . . . . 14
   

  

  

  |
10 | | eqtr 2054 |
. . . . . . . . . . . . . . . . . 18
            
    |
11 | | resco 4768 |
. . . . . . . . . . . . . . . . . . 19
       |
12 | | uneq1 3084 |
. . . . . . . . . . . . . . . . . . 19
     
             |
13 | | reseq1 4549 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
     |
14 | | eqtr 2054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              
      |
15 | 14 | uneq2d 3091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              

         |
16 | | eqtr 2054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
           

            
         |
17 | | resss 4578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
18 | | ssequn2 3110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
       |
19 | 17, 18 | mpbi 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
20 | 6, 19 | syl6reqr 2088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

   

  |
21 | | eqeq1 2043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 

            |
22 | 20, 21 | syl5ibr 145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                          |
23 | 16, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
           

        
 
  
       |
24 | 23 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               

         
           |
25 | 24 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
            
           |
26 | 15, 25 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                              
           |
27 | 26 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             
            |
28 | 27 | eqcoms 2040 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                        
            |
29 | 28 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . 22
           
                 
            |
30 | 13, 29 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
                 
            |
31 | 6, 30 | mpcom 32 |
. . . . . . . . . . . . . . . . . . . 20

  
 
                 
           |
32 | 31 | com3l 75 |
. . . . . . . . . . . . . . . . . . 19
    
                     
        |
33 | 11, 12, 32 | mpsyl 59 |
. . . . . . . . . . . . . . . . . 18
         
       |
34 | 10, 33 | syl 14 |
. . . . . . . . . . . . . . . . 17
              
          |
35 | 34 | ex 108 |
. . . . . . . . . . . . . . . 16
                
        |
36 | 35 | eqcoms 2040 |
. . . . . . . . . . . . . . 15
    
           
        |
37 | 36 | com3l 75 |
. . . . . . . . . . . . . 14
         
      
        |
38 | 9, 37 | syl 14 |
. . . . . . . . . . . . 13
   

  

    


 
 
           |
39 | 38 | ex 108 |
. . . . . . . . . . . 12
       

     
      
         |
40 | 39 | com3l 75 |
. . . . . . . . . . 11
 
            
      
         |
41 | 8, 40 | mpcom 32 |
. . . . . . . . . 10

  
       
      
        |
42 | 7, 41 | syl5com 26 |
. . . . . . . . 9
 
     
      
        |
43 | 6, 42 | mpcom 32 |
. . . . . . . 8

  
 
      
       |
44 | 5, 43 | mpi 15 |
. . . . . . 7

 
  
      |
45 | 4, 44 | syl5eq 2081 |
. . . . . 6

         |
46 | | eqeq1 2043 |
. . . . . 6
       
     
               |
47 | 45, 46 | syl5ibr 145 |
. . . . 5
       
              |
48 | 2, 3, 47 | mp2b 8 |
. . . 4


       |
49 | | reseq2 4550 |
. . . . . 6
       
     |
50 | 49 | coeq2d 4441 |
. . . . 5
     
   

      |
51 | 50 | eqeq1d 2045 |
. . . 4
                     |
52 | 48, 51 | syl5ibr 145 |
. . 3
          

   |
53 | 1, 52 | mpcom 32 |
. 2


       |
54 | 53, 6 | eqtrd 2069 |
1


      |