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


  
  |
2 | | eldifi 3125 |
. . . . . . . . 9
     |
3 | | ne0i 3295 |
. . . . . . . . 9
   |
4 | 2, 3 | syl 14 |
. . . . . . . 8
     |
5 | 4 | neneqd 2277 |
. . . . . . 7
  
  |
6 | 5 | ad2antlr 474 |
. . . . . 6
   


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


  
  |
8 | | php5dom 6635 |
. . . . . . . . . 10

  |
9 | 8 | ad2antlr 474 |
. . . . . . . . 9
             |
10 | | simplr 498 |
. . . . . . . . . 10
      
  

    |
11 | | simpr 109 |
. . . . . . . . . . 11
      
  

    |
12 | | vex 2625 |
. . . . . . . . . . . . . . . 16
 |
13 | 12 | sucex 4331 |
. . . . . . . . . . . . . . 15
 |
14 | | difss 3129 |
. . . . . . . . . . . . . . 15
     |
15 | 13, 14 | ssexi 3985 |
. . . . . . . . . . . . . 14
     |
16 | | eldifn 3126 |
. . . . . . . . . . . . . . . 16
  
  |
17 | 16 | ad3antlr 478 |
. . . . . . . . . . . . . . 15
          
  |
18 | | simpllr 502 |
. . . . . . . . . . . . . . . . 17
   


     |
19 | 18 | adantr 271 |
. . . . . . . . . . . . . . . 16
             |
20 | | simpr 109 |
. . . . . . . . . . . . . . . 16
          
  |
21 | 19, 20 | sseqtrd 3065 |
. . . . . . . . . . . . . . 15
             |
22 | | ssdif 3138 |
. . . . . . . . . . . . . . . 16

    
     |
23 | | disjsn 3510 |
. . . . . . . . . . . . . . . . . 18
    
  |
24 | | disj3 3341 |
. . . . . . . . . . . . . . . . . 18
           |
25 | 23, 24 | bitr3i 185 |
. . . . . . . . . . . . . . . . 17


     |
26 | | sseq1 3050 |
. . . . . . . . . . . . . . . . 17
         
           |
27 | 25, 26 | sylbi 120 |
. . . . . . . . . . . . . . . 16
  
  
           |
28 | 22, 27 | syl5ibr 155 |
. . . . . . . . . . . . . . 15
  
      |
29 | 17, 21, 28 | sylc 62 |
. . . . . . . . . . . . . 14
                 |
30 | | ssdomg 6551 |
. . . . . . . . . . . . . 14
                 |
31 | 15, 29, 30 | mpsyl 65 |
. . . . . . . . . . . . 13
                 |
32 | | simplr 498 |
. . . . . . . . . . . . . 14
             |
33 | 2 | ad3antlr 478 |
. . . . . . . . . . . . . . 15
          
  |
34 | 33, 20 | eleqtrd 2167 |
. . . . . . . . . . . . . 14
          
  |
35 | | phplem3g 6628 |
. . . . . . . . . . . . . . 15
 
 
     |
36 | 35 | ensymd 6556 |
. . . . . . . . . . . . . 14
 
       |
37 | 32, 34, 36 | syl2anc 404 |
. . . . . . . . . . . . 13
           
     |
38 | | domentr 6564 |
. . . . . . . . . . . . 13
             |
39 | 31, 37, 38 | syl2anc 404 |
. . . . . . . . . . . 12
             |
40 | 39 | adantr 271 |
. . . . . . . . . . 11
      
  

    |
41 | | endomtr 6563 |
. . . . . . . . . . 11
     |
42 | 11, 40, 41 | syl2anc 404 |
. . . . . . . . . 10
      
  

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

    |
44 | 9, 43 | mtand 627 |
. . . . . . . 8
          
  |
45 | 44 | ex 114 |
. . . . . . 7
   


   
   |
46 | 45 | rexlimdva 2491 |
. . . . . 6
  

    
   |
47 | 46 | imp 123 |
. . . . 5
   


      |
48 | | nn0suc 4434 |
. . . . . 6
 

   |
49 | 48 | ad2antrr 473 |
. . . . 5
  

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

  
  |
51 | 50 | ex 114 |
. . 3
     
   |
52 | 51 | exlimdv 1748 |
. 2
          |
53 | 52 | 3impia 1141 |
1
  
  
  |