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


  
  |
2 | | eldifi 3257 |
. . . . . . . . 9
     |
3 | | ne0i 3429 |
. . . . . . . . 9
   |
4 | 2, 3 | syl 14 |
. . . . . . . 8
     |
5 | 4 | neneqd 2368 |
. . . . . . 7
  
  |
6 | 5 | ad2antlr 489 |
. . . . . 6
   


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


  
  |
8 | | php5dom 6862 |
. . . . . . . . . 10

  |
9 | 8 | ad2antlr 489 |
. . . . . . . . 9
             |
10 | | simplr 528 |
. . . . . . . . . 10
      
  

    |
11 | | simpr 110 |
. . . . . . . . . . 11
      
  

    |
12 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
13 | 12 | sucex 4498 |
. . . . . . . . . . . . . . 15
 |
14 | | difss 3261 |
. . . . . . . . . . . . . . 15
     |
15 | 13, 14 | ssexi 4141 |
. . . . . . . . . . . . . 14
     |
16 | | eldifn 3258 |
. . . . . . . . . . . . . . . 16
  
  |
17 | 16 | ad3antlr 493 |
. . . . . . . . . . . . . . 15
          
  |
18 | | simpllr 534 |
. . . . . . . . . . . . . . . . 17
   


     |
19 | 18 | adantr 276 |
. . . . . . . . . . . . . . . 16
             |
20 | | simpr 110 |
. . . . . . . . . . . . . . . 16
          
  |
21 | 19, 20 | sseqtrd 3193 |
. . . . . . . . . . . . . . 15
             |
22 | | ssdif 3270 |
. . . . . . . . . . . . . . . 16

    
     |
23 | | disjsn 3654 |
. . . . . . . . . . . . . . . . . 18
    
  |
24 | | disj3 3475 |
. . . . . . . . . . . . . . . . . 18
           |
25 | 23, 24 | bitr3i 186 |
. . . . . . . . . . . . . . . . 17


     |
26 | | sseq1 3178 |
. . . . . . . . . . . . . . . . 17
         
           |
27 | 25, 26 | sylbi 121 |
. . . . . . . . . . . . . . . 16
  
  
           |
28 | 22, 27 | imbitrrid 156 |
. . . . . . . . . . . . . . 15
  
      |
29 | 17, 21, 28 | sylc 62 |
. . . . . . . . . . . . . 14
                 |
30 | | ssdomg 6777 |
. . . . . . . . . . . . . 14
                 |
31 | 15, 29, 30 | mpsyl 65 |
. . . . . . . . . . . . 13
                 |
32 | | simplr 528 |
. . . . . . . . . . . . . 14
             |
33 | 2 | ad3antlr 493 |
. . . . . . . . . . . . . . 15
          
  |
34 | 33, 20 | eleqtrd 2256 |
. . . . . . . . . . . . . 14
          
  |
35 | | phplem3g 6855 |
. . . . . . . . . . . . . . 15
 
 
     |
36 | 35 | ensymd 6782 |
. . . . . . . . . . . . . 14
 
       |
37 | 32, 34, 36 | syl2anc 411 |
. . . . . . . . . . . . 13
           
     |
38 | | domentr 6790 |
. . . . . . . . . . . . 13
             |
39 | 31, 37, 38 | syl2anc 411 |
. . . . . . . . . . . 12
             |
40 | 39 | adantr 276 |
. . . . . . . . . . 11
      
  

    |
41 | | endomtr 6789 |
. . . . . . . . . . 11
     |
42 | 11, 40, 41 | syl2anc 411 |
. . . . . . . . . 10
      
  

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

    |
44 | 9, 43 | mtand 665 |
. . . . . . . 8
          
  |
45 | 44 | ex 115 |
. . . . . . 7
   


   
   |
46 | 45 | rexlimdva 2594 |
. . . . . 6
  

    
   |
47 | 46 | imp 124 |
. . . . 5
   


      |
48 | | nn0suc 4603 |
. . . . . 6
 

   |
49 | 48 | ad2antrr 488 |
. . . . 5
  

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

  
  |
51 | 50 | ex 115 |
. . 3
     
   |
52 | 51 | exlimdv 1819 |
. 2
          |
53 | 52 | 3impia 1200 |
1
  
  
  |