Metamath Proof Explorer


Theorem frgrnbnb

Description: If two neighbors U and W of a vertex X have a common neighbor A in a friendship graph, then this common neighbor A must be the vertex X . (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses frgrnbnb.e E=EdgG
frgrnbnb.n D=GNeighbVtxX
Assertion frgrnbnb GFriendGraphUDWDUWUAEWAEA=X

Proof

Step Hyp Ref Expression
1 frgrnbnb.e E=EdgG
2 frgrnbnb.n D=GNeighbVtxX
3 frgrusgr GFriendGraphGUSGraph
4 2 eleq2i UDUGNeighbVtxX
5 1 nbusgreledg GUSGraphUGNeighbVtxXUXE
6 5 biimpd GUSGraphUGNeighbVtxXUXE
7 4 6 syl5bi GUSGraphUDUXE
8 2 eleq2i WDWGNeighbVtxX
9 1 nbusgreledg GUSGraphWGNeighbVtxXWXE
10 9 biimpd GUSGraphWGNeighbVtxXWXE
11 8 10 syl5bi GUSGraphWDWXE
12 7 11 anim12d GUSGraphUDWDUXEWXE
13 12 imp GUSGraphUDWDUXEWXE
14 eqid VtxG=VtxG
15 14 nbgrisvtx UGNeighbVtxXUVtxG
16 15 2 eleq2s UDUVtxG
17 14 nbgrisvtx WGNeighbVtxXWVtxG
18 17 2 eleq2s WDWVtxG
19 16 18 anim12i UDWDUVtxGWVtxG
20 19 adantl GUSGraphUDWDUVtxGWVtxG
21 1 14 usgrpredgv GUSGraphUAEUVtxGAVtxG
22 21 ad2ant2r GUSGraphUDWDUAEWAEUVtxGAVtxG
23 ax-1 A=XGFriendGraphA=X
24 23 2a1d A=XUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
25 24 2a1d A=XUWUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
26 simpll GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWGUSGraph
27 simprrr GUSGraphXVtxGAVtxGUVtxGWVtxGWVtxG
28 27 adantr GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWWVtxG
29 simprrl GUSGraphXVtxGAVtxGUVtxGWVtxGUVtxG
30 29 adantr GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWUVtxG
31 necom UWWU
32 31 biimpi UWWU
33 32 adantl AXUWWU
34 33 adantl GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWWU
35 28 30 34 3jca GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWWVtxGUVtxGWU
36 simprll GUSGraphXVtxGAVtxGUVtxGWVtxGXVtxG
37 36 adantr GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWXVtxG
38 simprlr GUSGraphXVtxGAVtxGUVtxGWVtxGAVtxG
39 38 adantr GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWAVtxG
40 necom AXXA
41 40 biimpi AXXA
42 41 adantr AXUWXA
43 42 adantl GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWXA
44 37 39 43 3jca GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWXVtxGAVtxGXA
45 26 35 44 3jca GUSGraphXVtxGAVtxGUVtxGWVtxGAXUWGUSGraphWVtxGUVtxGWUXVtxGAVtxGXA
46 45 ad4ant14 GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUWGUSGraphWVtxGUVtxGWUXVtxGAVtxGXA
47 prcom UX=XU
48 47 eleq1i UXEXUE
49 48 biimpi UXEXUE
50 49 anim1ci UXEWXEWXEXUE
51 50 adantl GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEWXEXUE
52 prcom WA=AW
53 52 eleq1i WAEAWE
54 53 biimpi WAEAWE
55 54 anim2i UAEWAEUAEAWE
56 51 55 anim12i GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEWXEXUEUAEAWE
57 56 adantr GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUWWXEXUEUAEAWE
58 14 1 4cyclusnfrgr GUSGraphWVtxGUVtxGWUXVtxGAVtxGXAWXEXUEUAEAWEGFriendGraph
59 46 57 58 sylc GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUWGFriendGraph
60 df-nel GFriendGraph¬GFriendGraph
61 59 60 sylib GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUW¬GFriendGraph
62 61 pm2.21d GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUWGFriendGraphA=X
63 62 ex GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEAXUWGFriendGraphA=X
64 63 com23 GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEGFriendGraphAXUWA=X
65 64 exp41 GUSGraphXVtxGAVtxGUVtxGWVtxGUXEWXEUAEWAEGFriendGraphAXUWA=X
66 65 com25 GUSGraphGFriendGraphUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGAXUWA=X
67 3 66 mpcom GFriendGraphUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGAXUWA=X
68 67 com15 AXUWUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
69 68 ex AXUWUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
70 25 69 pm2.61ine UWUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
71 70 imp UWUXEWXEUAEWAEXVtxGAVtxGUVtxGWVtxGGFriendGraphA=X
72 71 com13 XVtxGAVtxGUVtxGWVtxGUAEWAEUWUXEWXEGFriendGraphA=X
73 72 ex XVtxGAVtxGUVtxGWVtxGUAEWAEUWUXEWXEGFriendGraphA=X
74 73 com25 XVtxGAVtxGGFriendGraphUAEWAEUWUXEWXEUVtxGWVtxGA=X
75 74 ex XVtxGAVtxGGFriendGraphUAEWAEUWUXEWXEUVtxGWVtxGA=X
76 14 nbgrcl UGNeighbVtxXXVtxG
77 76 2 eleq2s UDXVtxG
78 77 adantr UDWDXVtxG
79 78 adantl GUSGraphUDWDXVtxG
80 75 79 syl11 AVtxGGUSGraphUDWDGFriendGraphUAEWAEUWUXEWXEUVtxGWVtxGA=X
81 80 com34 AVtxGGUSGraphUDWDUAEWAEGFriendGraphUWUXEWXEUVtxGWVtxGA=X
82 81 impd AVtxGGUSGraphUDWDUAEWAEGFriendGraphUWUXEWXEUVtxGWVtxGA=X
83 82 adantl UVtxGAVtxGGUSGraphUDWDUAEWAEGFriendGraphUWUXEWXEUVtxGWVtxGA=X
84 22 83 mpcom GUSGraphUDWDUAEWAEGFriendGraphUWUXEWXEUVtxGWVtxGA=X
85 84 ex GUSGraphUDWDUAEWAEGFriendGraphUWUXEWXEUVtxGWVtxGA=X
86 85 com25 GUSGraphUDWDUVtxGWVtxGGFriendGraphUWUXEWXEUAEWAEA=X
87 86 com14 UWUXEWXEUVtxGWVtxGGFriendGraphGUSGraphUDWDUAEWAEA=X
88 87 ex UWUXEWXEUVtxGWVtxGGFriendGraphGUSGraphUDWDUAEWAEA=X
89 88 com15 GUSGraphUDWDUXEWXEUVtxGWVtxGGFriendGraphUWUAEWAEA=X
90 13 20 89 mp2d GUSGraphUDWDGFriendGraphUWUAEWAEA=X
91 90 ex GUSGraphUDWDGFriendGraphUWUAEWAEA=X
92 91 com23 GUSGraphGFriendGraphUDWDUWUAEWAEA=X
93 3 92 mpcom GFriendGraphUDWDUWUAEWAEA=X
94 93 3imp GFriendGraphUDWDUWUAEWAEA=X