Proof of Theorem cnvrcl0
Step | Hyp | Ref
| Expression |
1 | | cnvresid 5663 |
. . . . . . 7


      |
2 | | cnvnonrel 36265 |
. . . . . . . . . . . . . . . 16
      |
3 | | cnv0 5245 |
. . . . . . . . . . . . . . . 16
  |
4 | 2, 3 | eqtr4i 2496 |
. . . . . . . . . . . . . . 15
       |
5 | 4 | dmeqi 5041 |
. . . . . . . . . . . . . 14
 
     |
6 | | df-rn 4850 |
. . . . . . . . . . . . . 14
     
    |
7 | | df-rn 4850 |
. . . . . . . . . . . . . 14
  |
8 | 5, 6, 7 | 3eqtr4i 2503 |
. . . . . . . . . . . . 13
     |
9 | | 0ss 3766 |
. . . . . . . . . . . . . 14
  |
10 | | rnss 5069 |
. . . . . . . . . . . . . 14
 
   |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
  |
12 | 8, 11 | eqsstri 3448 |
. . . . . . . . . . . 12
   
  |
13 | | ssequn2 3598 |
. . . . . . . . . . . 12
       
        |
14 | 12, 13 | mpbi 213 |
. . . . . . . . . . 11
 

      |
15 | | rnun 5250 |
. . . . . . . . . . 11
 
             |
16 | | dfdm4 5032 |
. . . . . . . . . . 11
  |
17 | 14, 15, 16 | 3eqtr4ri 2504 |
. . . . . . . . . 10
        |
18 | 4 | rneqi 5067 |
. . . . . . . . . . . . . 14
 
     |
19 | | dfdm4 5032 |
. . . . . . . . . . . . . 14
     
    |
20 | | dfdm4 5032 |
. . . . . . . . . . . . . 14
  |
21 | 18, 19, 20 | 3eqtr4i 2503 |
. . . . . . . . . . . . 13
     |
22 | | dmss 5039 |
. . . . . . . . . . . . . 14
 
   |
23 | 9, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
  |
24 | 21, 23 | eqsstri 3448 |
. . . . . . . . . . . 12
   
  |
25 | | ssequn2 3598 |
. . . . . . . . . . . 12
       
        |
26 | 24, 25 | mpbi 213 |
. . . . . . . . . . 11
 

      |
27 | | dmun 5047 |
. . . . . . . . . . 11
 
             |
28 | | df-rn 4850 |
. . . . . . . . . . 11
  |
29 | 26, 27, 28 | 3eqtr4ri 2504 |
. . . . . . . . . 10
        |
30 | 17, 29 | uneq12i 3577 |
. . . . . . . . 9
                   |
31 | 30 | equncomi 3571 |
. . . . . . . 8
                   |
32 | 31 | reseq2i 5108 |
. . . . . . 7
                     |
33 | 1, 32 | eqtr2i 2494 |
. . . . . 6
         
            |
34 | | cnvss 5012 |
. . . . . 6


 
 
     |
35 | 33, 34 | syl5eqss 3462 |
. . . . 5


 
  
      
          |
36 | | ssun1 3588 |
. . . . 5
         |
37 | 35, 36 | syl6ss 3430 |
. . . 4


 
  
      
                |
38 | | dmeq 5040 |
. . . . . . 7
         
       |
39 | | rneq 5066 |
. . . . . . 7
         
       |
40 | 38, 39 | uneq12d 3580 |
. . . . . 6
        
                   |
41 | 40 | reseq2d 5111 |
. . . . 5
          
  
      
         |
42 | | id 22 |
. . . . 5
       
 
       |
43 | 41, 42 | sseq12d 3447 |
. . . 4
           
  
      
                 |
44 | 37, 43 | syl5ibr 229 |
. . 3
         
        |
45 | 44 | adantl 473 |
. 2
 
 
                |
46 | | cnvresid 5663 |
. . . . . 6


      |
47 | | dfdm4 5032 |
. . . . . . . . 9
  |
48 | | df-rn 4850 |
. . . . . . . . 9
  |
49 | 47, 48 | uneq12i 3577 |
. . . . . . . 8
   
   |
50 | 49 | equncomi 3571 |
. . . . . . 7
   
   |
51 | 50 | reseq2i 5108 |
. . . . . 6
    
    |
52 | 46, 51 | eqtr2i 2494 |
. . . . 5
     

   |
53 | | cnvss 5012 |
. . . . 5


 
       |
54 | 52, 53 | syl5eqss 3462 |
. . . 4


 
        |
55 | | dmeq 5040 |
. . . . . . 7
 
   |
56 | | rneq 5066 |
. . . . . . 7
 
   |
57 | 55, 56 | uneq12d 3580 |
. . . . . 6
  
       |
58 | 57 | reseq2d 5111 |
. . . . 5
  
   
     |
59 | | id 22 |
. . . . 5
     |
60 | 58, 59 | sseq12d 3447 |
. . . 4
   
   
       |
61 | 54, 60 | syl5ibr 229 |
. . 3
      
     |
62 | 61 | adantl 473 |
. 2
 
 
          |
63 | | dmeq 5040 |
. . . . 5
 
    
      |
64 | | rneq 5066 |
. . . . 5
 
    
      |
65 | 63, 64 | uneq12d 3580 |
. . . 4
 
    
  
    
       |
66 | 65 | reseq2d 5111 |
. . 3
 
      
 
    
        |
67 | | id 22 |
. . 3
 
   

      |
68 | 66, 67 | sseq12d 3447 |
. 2
 
       
 
    
      
       |
69 | | ssun1 3588 |
. . 3

     |
70 | 69 | a1i 11 |
. 2
        |
71 | | dmexg 6743 |
. . . . 5
   |
72 | | rnexg 6744 |
. . . . 5
   |
73 | | unexg 6611 |
. . . . 5
 
     |
74 | 71, 72, 73 | syl2anc 673 |
. . . 4
     |
75 | 74 | resiexd 6147 |
. . 3
      |
76 | | unexg 6611 |
. . 3
 
    
      |
77 | 75, 76 | mpdan 681 |
. 2
 
      |
78 | | dmun 5047 |
. . . . . 6

          |
79 | | ssun1 3588 |
. . . . . . 7
   |
80 | | dmresi 5166 |
. . . . . . . 8
      |
81 | 80 | eqimssi 3472 |
. . . . . . 7
      |
82 | 79, 81 | unssi 3600 |
. . . . . 6
    
   |
83 | 78, 82 | eqsstri 3448 |
. . . . 5

       |
84 | | rnun 5250 |
. . . . . 6

          |
85 | | ssun2 3589 |
. . . . . . 7
   |
86 | | rnresi 5187 |
. . . . . . . 8
      |
87 | 86 | eqimssi 3472 |
. . . . . . 7
      |
88 | 85, 87 | unssi 3600 |
. . . . . 6
    
   |
89 | 84, 88 | eqsstri 3448 |
. . . . 5

       |
90 | 83, 89 | pm3.2i 462 |
. . . 4
     
           |
91 | | unss 3599 |
. . . . 5
  
      
       

    
         |
92 | | ssres2 5137 |
. . . . 5
  
    
             
           |
93 | 91, 92 | sylbi 200 |
. . . 4
  
      
             
           |
94 | | ssun4 3591 |
. . . 4

 
    
               
      
      |
95 | 90, 93, 94 | mp2b 10 |
. . 3
      
     

     |
96 | 95 | a1i 11 |
. 2
  
          

      |
97 | 45, 62, 68, 70, 77, 96 | clcnvlem 36301 |
1
    
        
       |