Proof of Theorem nbhashuvtx1
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
     Neighbors   

    Neighbors     |
2 | 1 | 2a1d 27 |
. 2
     Neighbors    USGrph
       
 Neighbors                Neighbors       |
3 | | df-nel 2636 |
. . 3
     Neighbors 
    Neighbors    |
4 | | nbgrassvwo2 25215 |
. . . . . . 7
  USGrph
    Neighbors       Neighbors         |
5 | 4 | ex 440 |
. . . . . 6
 USGrph      Neighbors      Neighbors 
        |
6 | 5 | 3ad2ant1 1035 |
. . . . 5
  USGrph
      Neighbors      Neighbors 
        |
7 | | difexg 4565 |
. . . . . . 7
        |
8 | 7 | 3ad2ant2 1036 |
. . . . . 6
  USGrph
        |
9 | | hashss 12618 |
. . . . . . 7
    
      Neighbors             
 Neighbors              |
10 | 9 | ex 440 |
. . . . . 6
         
 Neighbors 
            Neighbors               |
11 | 8, 10 | syl 17 |
. . . . 5
  USGrph
      Neighbors              Neighbors               |
12 | | simpl2 1018 |
. . . . . . . . . . . 12
   USGrph
 
    |
13 | | simpl 463 |
. . . . . . . . . . . . 13
  
  |
14 | | simp3 1016 |
. . . . . . . . . . . . 13
  USGrph
   |
15 | | prssi 4141 |
. . . . . . . . . . . . 13
 
      |
16 | 13, 14, 15 | syl2anr 485 |
. . . . . . . . . . . 12
   USGrph
 
    
  |
17 | | hashssdif 12621 |
. . . . . . . . . . . 12
                              |
18 | 12, 16, 17 | syl2anc 671 |
. . . . . . . . . . 11
   USGrph
 
                          |
19 | | simprr 771 |
. . . . . . . . . . . . 13
   USGrph
 
    |
20 | | hashprg 12604 |
. . . . . . . . . . . . . 14
 
            |
21 | 13, 14, 20 | syl2anr 485 |
. . . . . . . . . . . . 13
   USGrph
 
       
     |
22 | 19, 21 | mpbid 215 |
. . . . . . . . . . . 12
   USGrph
 
      
    |
23 | 22 | oveq2d 6331 |
. . . . . . . . . . 11
   USGrph
 
                       |
24 | 18, 23 | eqtrd 2496 |
. . . . . . . . . 10
   USGrph
 
                   |
25 | 24 | breq2d 4428 |
. . . . . . . . 9
   USGrph
 
          Neighbors           
       Neighbors            |
26 | | nbhashnn0 25691 |
. . . . . . . . . . . . . 14
  USGrph
        Neighbors     |
27 | 26 | nn0zd 11067 |
. . . . . . . . . . . . 13
  USGrph
        Neighbors     |
28 | | hashcl 12570 |
. . . . . . . . . . . . . . 15
       |
29 | | nn0z 10989 |
. . . . . . . . . . . . . . 15
    
      |
30 | | peano2zm 11009 |
. . . . . . . . . . . . . . 15
    
        |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
         |
32 | 31 | 3ad2ant2 1036 |
. . . . . . . . . . . . 13
  USGrph
         |
33 | | zltlem1 11018 |
. . . . . . . . . . . . 13
         Neighbors                  Neighbors        
       Neighbors              |
34 | 27, 32, 33 | syl2anc 671 |
. . . . . . . . . . . 12
  USGrph
       
 Neighbors        
       Neighbors              |
35 | 28 | nn0cnd 10956 |
. . . . . . . . . . . . . . . 16
       |
36 | 35 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . 15
  USGrph
       |
37 | | 1cnd 9685 |
. . . . . . . . . . . . . . 15
  USGrph
   |
38 | 36, 37, 37 | subsub4d 10043 |
. . . . . . . . . . . . . 14
  USGrph
                   |
39 | | 1p1e2 10751 |
. . . . . . . . . . . . . . 15
   |
40 | 39 | oveq2i 6326 |
. . . . . . . . . . . . . 14
               |
41 | 38, 40 | syl6eq 2512 |
. . . . . . . . . . . . 13
  USGrph
                 |
42 | 41 | breq2d 4428 |
. . . . . . . . . . . 12
  USGrph
       
 Neighbors          
       Neighbors            |
43 | 34, 42 | bitrd 261 |
. . . . . . . . . . 11
  USGrph
       
 Neighbors        
       Neighbors            |
44 | 43 | adantr 471 |
. . . . . . . . . 10
   USGrph
 
          Neighbors              
 Neighbors            |
45 | 26 | nn0red 10955 |
. . . . . . . . . . . . . . 15
  USGrph
        Neighbors     |
46 | 45 | adantr 471 |
. . . . . . . . . . . . . 14
   USGrph
 
         Neighbors     |
47 | 46 | adantr 471 |
. . . . . . . . . . . . 13
    USGrph
         
 Neighbors                 Neighbors     |
48 | | simpr 467 |
. . . . . . . . . . . . 13
    USGrph
         
 Neighbors                 Neighbors           |
49 | 47, 48 | ltned 9797 |
. . . . . . . . . . . 12
    USGrph
         
 Neighbors                 Neighbors           |
50 | 49 | ex 440 |
. . . . . . . . . . 11
   USGrph
 
          Neighbors                Neighbors            |
51 | | eqneqall 2646 |
. . . . . . . . . . . 12
        Neighbors                 Neighbors        
    Neighbors     |
52 | 51 | com12 32 |
. . . . . . . . . . 11
        Neighbors                 Neighbors             Neighbors     |
53 | 50, 52 | syl6 34 |
. . . . . . . . . 10
   USGrph
 
          Neighbors                 Neighbors             Neighbors      |
54 | 44, 53 | sylbird 243 |
. . . . . . . . 9
   USGrph
 
          Neighbors                 Neighbors             Neighbors      |
55 | 25, 54 | sylbid 223 |
. . . . . . . 8
   USGrph
 
          Neighbors                    Neighbors             Neighbors      |
56 | 55 | ex 440 |
. . . . . . 7
  USGrph
  

        Neighbors                    Neighbors             Neighbors       |
57 | 56 | com23 81 |
. . . . . 6
  USGrph
       
 Neighbors             

        Neighbors             Neighbors       |
58 | 57 | com34 86 |
. . . . 5
  USGrph
       
 Neighbors                  
 Neighbors                Neighbors       |
59 | 6, 11, 58 | 3syld 57 |
. . . 4
  USGrph
      Neighbors        
 Neighbors                Neighbors       |
60 | 59 | com12 32 |
. . 3
     Neighbors    USGrph
       
 Neighbors                Neighbors       |
61 | 3, 60 | sylbir 218 |
. 2
   
 Neighbors 
  USGrph
       
 Neighbors                Neighbors       |
62 | 2, 61 | pm2.61i 169 |
1
  USGrph
       
 Neighbors                Neighbors      |