Proof of Theorem frgrancvvdeqlem3
Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeq.f |
. . . 4
 FriendGrph   |
2 | 1 | adantr 467 |
. . 3
 
 FriendGrph   |
3 | | frgrancvvdeq.nx |
. . . . . . 7
    Neighbors   |
4 | 3 | eleq2i 2521 |
. . . . . 6

    Neighbors    |
5 | | frisusgra 25720 |
. . . . . . 7
 FriendGrph USGrph
  |
6 | | nbgraisvtx 25159 |
. . . . . . 7
 USGrph      Neighbors     |
7 | 1, 5, 6 | 3syl 18 |
. . . . . 6
      Neighbors 
   |
8 | 4, 7 | syl5bi 221 |
. . . . 5
     |
9 | 8 | imp 431 |
. . . 4
 
   |
10 | | frgrancvvdeq.y |
. . . . 5
   |
11 | 10 | adantr 467 |
. . . 4
 
   |
12 | | frgrancvvdeq.ny |
. . . . . 6
    Neighbors   |
13 | | frgrancvvdeq.x |
. . . . . 6
   |
14 | | frgrancvvdeq.ne |
. . . . . 6
   |
15 | | frgrancvvdeq.xy |
. . . . . 6
   |
16 | | frgrancvvdeq.a |
. . . . . 6
         |
17 | 3, 12, 13, 10, 14, 15, 1, 16 | frgrancvvdeqlem1 25758 |
. . . . 5
 
       |
18 | | eldif 3414 |
. . . . . 6
           |
19 | | ssnid 3997 |
. . . . . . . . 9
   |
20 | | eleq1 2517 |
. . . . . . . . . 10
 
       |
21 | 20 | eqcoms 2459 |
. . . . . . . . 9
 
       |
22 | 19, 21 | mpbiri 237 |
. . . . . . . 8
     |
23 | 22 | necon3bi 2650 |
. . . . . . 7
     |
24 | 23 | adantl 468 |
. . . . . 6
 
     |
25 | 18, 24 | sylbi 199 |
. . . . 5
       |
26 | 17, 25 | syl 17 |
. . . 4
 
   |
27 | 9, 11, 26 | 3jca 1188 |
. . 3
 
 
   |
28 | | frgraunss 25723 |
. . 3
 FriendGrph  
 
            |
29 | 2, 27, 28 | sylc 62 |
. 2
 
 
           |
30 | | prex 4642 |
. . . . . . . . . . . 12
    |
31 | | prex 4642 |
. . . . . . . . . . . 12
    |
32 | 30, 31 | prss 4126 |
. . . . . . . . . . 11
       
            |
33 | | simpr 463 |
. . . . . . . . . . 11
       
      |
34 | 32, 33 | sylbir 217 |
. . . . . . . . . 10
         
     |
35 | 34 | ad2antll 735 |
. . . . . . . . 9
                     |
36 | 12 | a1i 11 |
. . . . . . . . . . . . 13
   
 Neighbors    |
37 | 36 | eleq2d 2514 |
. . . . . . . . . . . 12
      Neighbors     |
38 | | nbgraeledg 25158 |
. . . . . . . . . . . . 13
 USGrph      Neighbors 
      |
39 | 1, 5, 38 | 3syl 18 |
. . . . . . . . . . . 12
      Neighbors    
   |
40 | 37, 39 | bitrd 257 |
. . . . . . . . . . 11
        |
41 | 40 | adantr 467 |
. . . . . . . . . 10
 
 
      |
42 | 41 | adantr 467 |
. . . . . . . . 9
                   
   |
43 | 35, 42 | mpbird 236 |
. . . . . . . 8
                  |
44 | | simpl 459 |
. . . . . . . . . 10
       
      |
45 | 32, 44 | sylbir 217 |
. . . . . . . . 9
         
     |
46 | 45 | ad2antll 735 |
. . . . . . . 8
                     |
47 | 43, 46 | jca 535 |
. . . . . . 7
                       |
48 | 47 | ex 436 |
. . . . . 6
 
                     |
49 | 12 | eleq2i 2521 |
. . . . . . . . . . . . 13

    Neighbors    |
50 | 49, 39 | syl5bb 261 |
. . . . . . . . . . . 12
        |
51 | 50 | biimpd 211 |
. . . . . . . . . . 11
    
   |
52 | 51 | adantr 467 |
. . . . . . . . . 10
 
    
   |
53 | 52 | impcom 432 |
. . . . . . . . 9
       
  |
54 | | nbgraisvtx 25159 |
. . . . . . . . . . . . . . . 16
 USGrph      Neighbors     |
55 | 1, 5, 54 | 3syl 18 |
. . . . . . . . . . . . . . 15
      Neighbors 
   |
56 | 49, 55 | syl5bi 221 |
. . . . . . . . . . . . . 14
     |
57 | 56 | adantr 467 |
. . . . . . . . . . . . 13
 
     |
58 | 57 | impcom 432 |
. . . . . . . . . . . 12
       |
59 | 58 | ad2antlr 733 |
. . . . . . . . . . 11
                 |
60 | | simpl 459 |
. . . . . . . . . . . . 13
    
          |
61 | | id 22 |
. . . . . . . . . . . . 13
         |
62 | 60, 61 | anim12ci 571 |
. . . . . . . . . . . 12
                         |
63 | 62, 32 | sylib 200 |
. . . . . . . . . . 11
                       
  |
64 | 59, 63 | jca 535 |
. . . . . . . . . 10
                            |
65 | 64 | ex 436 |
. . . . . . . . 9
    
        

             |
66 | 53, 65 | mpancom 675 |
. . . . . . . 8
                       |
67 | 66 | impancom 442 |
. . . . . . 7
                       |
68 | 67 | com12 32 |
. . . . . 6
 
      

             |
69 | 48, 68 | impbid 194 |
. . . . 5
 
                     |
70 | 69 | eubidv 2319 |
. . . 4
 
              
          |
71 | 70 | biimpd 211 |
. . 3
 
                         |
72 | | df-reu 2744 |
. . 3
          
               |
73 | | df-reu 2744 |
. . 3
    
         |
74 | 71, 72, 73 | 3imtr4g 274 |
. 2
 
  
        
       |
75 | 29, 74 | mpd 15 |
1
 
 
     |