Step | Hyp | Ref
| Expression |
1 | | mopni.1 |
. . . . . 6
     |
2 | 1 | mopnuni 21456 |
. . . . 5
         |
3 | 2 | 3ad2ant1 1029 |
. . . 4
      
    |
4 | 3 | difeq1d 3550 |
. . 3
      
        |
5 | | difssd 3561 |
. . . 4
      
  
  |
6 | | simpl3 1013 |
. . . . . . 7
       
   
  |
7 | | simpl1 1011 |
. . . . . . . 8
       
   
       |
8 | | simpl2 1012 |
. . . . . . . 8
       
   
  |
9 | | eldifi 3555 |
. . . . . . . . 9
     |
10 | 9 | adantl 468 |
. . . . . . . 8
       
   
  |
11 | | xmetcl 21346 |
. . . . . . . 8
      

      |
12 | 7, 8, 10, 11 | syl3anc 1268 |
. . . . . . 7
       
   
      |
13 | | eldif 3414 |
. . . . . . . . . 10
  

   |
14 | | oveq2 6298 |
. . . . . . . . . . . . . 14
           |
15 | 14 | breq1d 4412 |
. . . . . . . . . . . . 13
     
       |
16 | | blcld.3 |
. . . . . . . . . . . . 13
       |
17 | 15, 16 | elrab2 3198 |
. . . . . . . . . . . 12


       |
18 | 17 | simplbi2 631 |
. . . . . . . . . . 11
     
   |
19 | 18 | con3dimp 443 |
. . . . . . . . . 10
 

      |
20 | 13, 19 | sylbi 199 |
. . . . . . . . 9
         |
21 | 20 | adantl 468 |
. . . . . . . 8
       
   
      |
22 | | xrltnle 9701 |
. . . . . . . . 9
           
       |
23 | 6, 12, 22 | syl2anc 667 |
. . . . . . . 8
       
   
    
       |
24 | 21, 23 | mpbird 236 |
. . . . . . 7
       
   
      |
25 | | qbtwnxr 11493 |
. . . . . . 7
     
    
 
       |
26 | 6, 12, 24, 25 | syl3anc 1268 |
. . . . . 6
       
   
 
       |
27 | | qre 11269 |
. . . . . . . 8
   |
28 | 7 | adantr 467 |
. . . . . . . . . . 11
        
     
      
       |
29 | 10 | adantr 467 |
. . . . . . . . . . 11
        
     
      
  |
30 | 12 | adantr 467 |
. . . . . . . . . . . 12
        
     
      
      |
31 | | rexr 9686 |
. . . . . . . . . . . . . 14
   |
32 | 31 | ad2antrl 734 |
. . . . . . . . . . . . 13
        
     
      
  |
33 | 32 | xnegcld 11586 |
. . . . . . . . . . . 12
        
     
      
    |
34 | 30, 33 | xaddcld 11587 |
. . . . . . . . . . 11
        
     
      
            |
35 | | blelrn 21432 |
. . . . . . . . . . 11
                                          |
36 | 28, 29, 34, 35 | syl3anc 1268 |
. . . . . . . . . 10
        
     
      
                        |
37 | | simprrr 775 |
. . . . . . . . . . . 12
        
     
      
      |
38 | | xposdif 11548 |
. . . . . . . . . . . . 13
       
   
             |
39 | 32, 30, 38 | syl2anc 667 |
. . . . . . . . . . . 12
        
     
      
                  |
40 | 37, 39 | mpbid 214 |
. . . . . . . . . . 11
        
     
      
            |
41 | | xblcntr 21426 |
. . . . . . . . . . 11
                             
                    |
42 | 28, 29, 34, 40, 41 | syl112anc 1272 |
. . . . . . . . . 10
        
     
      
                    |
43 | | incom 3625 |
. . . . . . . . . . . . 13
                                                         |
44 | 8 | adantr 467 |
. . . . . . . . . . . . . 14
        
     
      
  |
45 | | xaddcom 11531 |
. . . . . . . . . . . . . . . . 17
                                             |
46 | 32, 34, 45 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
        
     
      
                                |
47 | | simprl 764 |
. . . . . . . . . . . . . . . . 17
        
     
      
  |
48 | | xnpcan 11538 |
. . . . . . . . . . . . . . . . 17
                            |
49 | 30, 47, 48 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
        
     
      
                     |
50 | 46, 49 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
        
     
      
                     |
51 | | xrleid 11449 |
. . . . . . . . . . . . . . . 16
    
          |
52 | 30, 51 | syl 17 |
. . . . . . . . . . . . . . 15
        
     
      
          |
53 | 50, 52 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
        
     
      
                     |
54 | | bldisj 21413 |
. . . . . . . . . . . . . 14
       

                                                              |
55 | 28, 44, 29, 32, 34, 53, 54 | syl33anc 1283 |
. . . . . . . . . . . . 13
        
     
      
                              |
56 | 43, 55 | syl5eq 2497 |
. . . . . . . . . . . 12
        
     
      
                              |
57 | | blssm 21433 |
. . . . . . . . . . . . . 14
                                      |
58 | 28, 29, 34, 57 | syl3anc 1268 |
. . . . . . . . . . . . 13
        
     
      
                    |
59 | | reldisj 3808 |
. . . . . . . . . . . . 13
                                               
                               |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
        
     
      
                            
                               |
61 | 56, 60 | mpbid 214 |
. . . . . . . . . . 11
        
     
      
                              |
62 | 6 | adantr 467 |
. . . . . . . . . . . . 13
        
     
      
  |
63 | | simprrl 774 |
. . . . . . . . . . . . 13
        
     
      
  |
64 | 1, 16 | blsscls2 21519 |
. . . . . . . . . . . . 13
       
 
            |
65 | 28, 44, 62, 32, 63, 64 | syl23anc 1275 |
. . . . . . . . . . . 12
        
     
      
          |
66 | 65 | sscond 3570 |
. . . . . . . . . . 11
        
     
      
         
    |
67 | 61, 66 | sstrd 3442 |
. . . . . . . . . 10
        
     
      
                      |
68 | | eleq2 2518 |
. . . . . . . . . . . 12
                                         |
69 | | sseq1 3453 |
. . . . . . . . . . . 12
                    
                   
    |
70 | 68, 69 | anbi12d 717 |
. . . . . . . . . . 11
                       
                                     
     |
71 | 70 | rspcev 3150 |
. . . . . . . . . 10
                       
                                     
          
    |
72 | 36, 42, 67, 71 | syl12anc 1266 |
. . . . . . . . 9
        
     
      
       
    |
73 | 72 | expr 620 |
. . . . . . . 8
        
      
           
      |
74 | 27, 73 | sylan2 477 |
. . . . . . 7
        
      
           
      |
75 | 74 | rexlimdva 2879 |
. . . . . 6
       
   
 
             
     |
76 | 26, 75 | mpd 15 |
. . . . 5
       
   
       
    |
77 | 76 | ralrimiva 2802 |
. . . 4
      
           
     |
78 | 1 | elmopn 21457 |
. . . . 5
        
              
      |
79 | 78 | 3ad2ant1 1029 |
. . . 4
      
      
                  |
80 | 5, 77, 79 | mpbir2and 933 |
. . 3
      
     |
81 | 4, 80 | eqeltrrd 2530 |
. 2
      
      |
82 | 1 | mopntop 21455 |
. . . 4
        |
83 | 82 | 3ad2ant1 1029 |
. . 3
      
   |
84 | | ssrab2 3514 |
. . . . 5
       |
85 | 16, 84 | eqsstri 3462 |
. . . 4
 |
86 | 85, 3 | syl5sseq 3480 |
. . 3
      

   |
87 | | eqid 2451 |
. . . 4
   |
88 | 87 | iscld2 20043 |
. . 3
               |
89 | 83, 86, 88 | syl2anc 667 |
. 2
      
            |
90 | 81, 89 | mpbird 236 |
1
      
       |