Metamath Proof Explorer


Theorem frgrncvvdeqlem7

Description: Lemma 7 for frgrncvvdeq . This corresponds to statement 1 in Huneke p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021)

Ref Expression
Hypotheses frgrncvvdeq.v1 V=VtxG
frgrncvvdeq.e E=EdgG
frgrncvvdeq.nx D=GNeighbVtxX
frgrncvvdeq.ny N=GNeighbVtxY
frgrncvvdeq.x φXV
frgrncvvdeq.y φYV
frgrncvvdeq.ne φXY
frgrncvvdeq.xy φYD
frgrncvvdeq.f φGFriendGraph
frgrncvvdeq.a A=xDιyN|xyE
Assertion frgrncvvdeqlem7 φxDAxX

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 V=VtxG
2 frgrncvvdeq.e E=EdgG
3 frgrncvvdeq.nx D=GNeighbVtxX
4 frgrncvvdeq.ny N=GNeighbVtxY
5 frgrncvvdeq.x φXV
6 frgrncvvdeq.y φYV
7 frgrncvvdeq.ne φXY
8 frgrncvvdeq.xy φYD
9 frgrncvvdeq.f φGFriendGraph
10 frgrncvvdeq.a A=xDιyN|xyE
11 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem5 φxDAx=GNeighbVtxxN
12 fvex AxV
13 12 snid AxAx
14 eleq2 Ax=GNeighbVtxxNAxAxAxGNeighbVtxxN
15 14 biimpa Ax=GNeighbVtxxNAxAxAxGNeighbVtxxN
16 elin AxGNeighbVtxxNAxGNeighbVtxxAxN
17 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 φXN
18 df-nel XN¬XN
19 nelelne ¬XNAxNAxX
20 18 19 sylbi XNAxNAxX
21 17 20 syl φAxNAxX
22 21 adantr φxDAxNAxX
23 22 com12 AxNφxDAxX
24 16 23 simplbiim AxGNeighbVtxxNφxDAxX
25 15 24 syl Ax=GNeighbVtxxNAxAxφxDAxX
26 13 25 mpan2 Ax=GNeighbVtxxNφxDAxX
27 11 26 mpcom φxDAxX
28 27 ralrimiva φxDAxX