Step | Hyp | Ref
| Expression |
1 | | dedekindeu.lss |
. . 3

  |
2 | | dedekindeu.uss |
. . 3

  |
3 | | dedekindeu.lm |
. . 3
 
  |
4 | | dedekindeu.um |
. . 3
 
  |
5 | | dedekindeu.lr |
. . 3
       |
6 | | dedekindeu.ur |
. . 3
       |
7 | | dedekindeu.disj |
. . 3
     |
8 | | dedekindeu.loc |
. . 3
   

    |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | dedekindeulemlub 13765 |
. 2
   
 
     |
10 | | simpr 110 |
. . . . . . . 8
   
  
 

  
   |
11 | 1 | ad3antrrr 492 |
. . . . . . . . . 10
   
  
 

  

  |
12 | 11, 10 | sseldd 3156 |
. . . . . . . . 9
   
  
 

  
   |
13 | | rsp 2524 |
. . . . . . . . . . 11
 





     |
14 | 5, 13 | syl 14 |
. . . . . . . . . 10
        |
15 | 14 | ad3antrrr 492 |
. . . . . . . . 9
   
  
 

  
        |
16 | 12, 15 | mpd 13 |
. . . . . . . 8
   
  
 

  
      |
17 | 10, 16 | mpbid 147 |
. . . . . . 7
   
  
 

  
    |
18 | 12 | adantr 276 |
. . . . . . . 8
       
 

  
 
 
  |
19 | 11 | adantr 276 |
. . . . . . . . 9
       
 

  
 
 
  |
20 | | simprl 529 |
. . . . . . . . 9
       
 

  
 
 
  |
21 | 19, 20 | sseldd 3156 |
. . . . . . . 8
       
 

  
 
 
  |
22 | | simp-4r 542 |
. . . . . . . 8
       
 

  
 
 
  |
23 | | simprr 531 |
. . . . . . . 8
       
 

  
 
 
  |
24 | | breq2 4004 |
. . . . . . . . . . 11
 
   |
25 | 24 | notbid 667 |
. . . . . . . . . 10
 
   |
26 | | simprl 529 |
. . . . . . . . . . 11
     
 
   

  |
27 | 26 | ad2antrr 488 |
. . . . . . . . . 10
       
 

  
 
 

  |
28 | 25, 27, 20 | rspcdva 2846 |
. . . . . . . . 9
       
 

  
 
 
  |
29 | 21, 22, 28 | nltled 8068 |
. . . . . . . 8
       
 

  
 
 
  |
30 | 18, 21, 22, 23, 29 | ltletrd 8370 |
. . . . . . 7
       
 

  
 
 
  |
31 | 17, 30 | rexlimddv 2599 |
. . . . . 6
   
  
 

  
   |
32 | 31 | ralrimiva 2550 |
. . . . 5
     
 
   

  |
33 | | simpr 110 |
. . . . . . . 8
   
  
 

  
   |
34 | | simplll 533 |
. . . . . . . . 9
   
  
 

  
   |
35 | 34, 2 | syl 14 |
. . . . . . . . . 10
   
  
 

  

  |
36 | 35, 33 | sseldd 3156 |
. . . . . . . . 9
   
  
 

  
   |
37 | | rsp 2524 |
. . . . . . . . . 10
 





     |
38 | 6, 37 | syl 14 |
. . . . . . . . 9
        |
39 | 34, 36, 38 | sylc 62 |
. . . . . . . 8
   
  
 

  
      |
40 | 33, 39 | mpbid 147 |
. . . . . . 7
   
  
 

  
    |
41 | | simp-4r 542 |
. . . . . . . 8
       
 

  
 
 
  |
42 | 35 | adantr 276 |
. . . . . . . . 9
       
 

  
 
 
  |
43 | | simprl 529 |
. . . . . . . . 9
       
 

  
 
 
  |
44 | 42, 43 | sseldd 3156 |
. . . . . . . 8
       
 

  
 
 
  |
45 | 36 | adantr 276 |
. . . . . . . 8
       
 

  
 
 
  |
46 | 43 | adantr 276 |
. . . . . . . . . 10
     

 
 
        
  |
47 | 34 | ad2antrr 488 |
. . . . . . . . . . 11
     

 
 
        
  |
48 | | simpr 110 |
. . . . . . . . . . . . . 14
     

 
 
        
  |
49 | | breq1 4003 |
. . . . . . . . . . . . . . . 16
 
   |
50 | | breq1 4003 |
. . . . . . . . . . . . . . . . 17
 
   |
51 | 50 | rexbidv 2478 |
. . . . . . . . . . . . . . . 16
  

   |
52 | 49, 51 | imbi12d 234 |
. . . . . . . . . . . . . . 15
    


    |
53 | | simprr 531 |
. . . . . . . . . . . . . . . 16
     
 
   
 

   |
54 | 53 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     

 
 
        
 

   |
55 | 44 | adantr 276 |
. . . . . . . . . . . . . . 15
     

 
 
        
  |
56 | 52, 54, 55 | rspcdva 2846 |
. . . . . . . . . . . . . 14
     

 
 
        


   |
57 | 48, 56 | mpd 13 |
. . . . . . . . . . . . 13
     

 
 
        

  |
58 | | breq2 4004 |
. . . . . . . . . . . . . 14
 
   |
59 | 58 | cbvrexv 2704 |
. . . . . . . . . . . . 13
 

  |
60 | 57, 59 | sylib 122 |
. . . . . . . . . . . 12
     

 
 
        

  |
61 | 47, 55, 14 | sylc 62 |
. . . . . . . . . . . 12
     

 
 
        

    |
62 | 60, 61 | mpbird 167 |
. . . . . . . . . . 11
     

 
 
        
  |
63 | | disj 3471 |
. . . . . . . . . . . . 13
  

  |
64 | 7, 63 | sylib 122 |
. . . . . . . . . . . 12
 
  |
65 | 64 | r19.21bi 2565 |
. . . . . . . . . . 11
 

  |
66 | 47, 62, 65 | syl2anc 411 |
. . . . . . . . . 10
     

 
 
        
  |
67 | 46, 66 | pm2.65da 661 |
. . . . . . . . 9
       
 

  
 
 
  |
68 | 41, 44, 67 | nltled 8068 |
. . . . . . . 8
       
 

  
 
 
  |
69 | | simprr 531 |
. . . . . . . 8
       
 

  
 
 
  |
70 | 41, 44, 45, 68, 69 | lelttrd 8072 |
. . . . . . 7
       
 

  
 
 
  |
71 | 40, 70 | rexlimddv 2599 |
. . . . . 6
   
  
 

  
   |
72 | 71 | ralrimiva 2550 |
. . . . 5
     
 
   

  |
73 | 32, 72 | jca 306 |
. . . 4
     
 
   
 

   |
74 | 73 | ex 115 |
. . 3
 

  
 
    
     |
75 | 74 | reximdva 2579 |
. 2
    
 

    
     |
76 | 9, 75 | mpd 13 |
1
    
   |