Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . . 6
   


  
  |
2 | | eldifi 3066 |
. . . . . . . . 9
     |
3 | | ne0i 3230 |
. . . . . . . . 9
   |
4 | 2, 3 | syl 14 |
. . . . . . . 8
     |
5 | 4 | neneqd 2226 |
. . . . . . 7
  
  |
6 | 5 | ad2antlr 458 |
. . . . . 6
   


  
  |
7 | 1, 6 | pm2.21dd 550 |
. . . . 5
   


  
  |
8 | | php5dom 6325 |
. . . . . . . . . 10

  |
9 | 8 | ad2antlr 458 |
. . . . . . . . 9
             |
10 | | simplr 482 |
. . . . . . . . . 10
      
  

    |
11 | | simpr 103 |
. . . . . . . . . . 11
      
  

    |
12 | | vex 2560 |
. . . . . . . . . . . . . . . 16
 |
13 | 12 | sucex 4225 |
. . . . . . . . . . . . . . 15
 |
14 | | difss 3070 |
. . . . . . . . . . . . . . 15
     |
15 | 13, 14 | ssexi 3895 |
. . . . . . . . . . . . . 14
     |
16 | | eldifn 3067 |
. . . . . . . . . . . . . . . 16
  
  |
17 | 16 | ad3antlr 462 |
. . . . . . . . . . . . . . 15
          
  |
18 | | simpllr 486 |
. . . . . . . . . . . . . . . . 17
   


     |
19 | 18 | adantr 261 |
. . . . . . . . . . . . . . . 16
             |
20 | | simpr 103 |
. . . . . . . . . . . . . . . 16
          
  |
21 | 19, 20 | sseqtrd 2981 |
. . . . . . . . . . . . . . 15
             |
22 | | ssdif 3078 |
. . . . . . . . . . . . . . . 16

    
     |
23 | | disjsn 3432 |
. . . . . . . . . . . . . . . . . 18
    
  |
24 | | disj3 3272 |
. . . . . . . . . . . . . . . . . 18
           |
25 | 23, 24 | bitr3i 175 |
. . . . . . . . . . . . . . . . 17


     |
26 | | sseq1 2966 |
. . . . . . . . . . . . . . . . 17
         
           |
27 | 25, 26 | sylbi 114 |
. . . . . . . . . . . . . . . 16
  
  
           |
28 | 22, 27 | syl5ibr 145 |
. . . . . . . . . . . . . . 15
  
      |
29 | 17, 21, 28 | sylc 56 |
. . . . . . . . . . . . . 14
                 |
30 | | ssdomg 6258 |
. . . . . . . . . . . . . 14
                 |
31 | 15, 29, 30 | mpsyl 59 |
. . . . . . . . . . . . 13
                 |
32 | | simplr 482 |
. . . . . . . . . . . . . 14
             |
33 | 2 | ad3antlr 462 |
. . . . . . . . . . . . . . 15
          
  |
34 | 33, 20 | eleqtrd 2116 |
. . . . . . . . . . . . . 14
          
  |
35 | | phplem3g 6319 |
. . . . . . . . . . . . . . 15
 
 
     |
36 | 35 | ensymd 6263 |
. . . . . . . . . . . . . 14
 
       |
37 | 32, 34, 36 | syl2anc 391 |
. . . . . . . . . . . . 13
           
     |
38 | | domentr 6271 |
. . . . . . . . . . . . 13
             |
39 | 31, 37, 38 | syl2anc 391 |
. . . . . . . . . . . 12
             |
40 | 39 | adantr 261 |
. . . . . . . . . . 11
      
  

    |
41 | | endomtr 6270 |
. . . . . . . . . . 11
     |
42 | 11, 40, 41 | syl2anc 391 |
. . . . . . . . . 10
      
  

    |
43 | 10, 42 | eqbrtrrd 3786 |
. . . . . . . . 9
      
  

    |
44 | 9, 43 | mtand 591 |
. . . . . . . 8
          
  |
45 | 44 | ex 108 |
. . . . . . 7
   


   
   |
46 | 45 | rexlimdva 2433 |
. . . . . 6
  

    
   |
47 | 46 | imp 115 |
. . . . 5
   


      |
48 | | nn0suc 4327 |
. . . . . 6
 

   |
49 | 48 | ad2antrr 457 |
. . . . 5
  

        |
50 | 7, 47, 49 | mpjaodan 711 |
. . . 4
  

  
  |
51 | 50 | ex 108 |
. . 3
     
   |
52 | 51 | exlimdv 1700 |
. 2
          |
53 | 52 | 3impia 1101 |
1
  
  
  |