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 | |
|
frgrncvvdeq.e | |
||
frgrncvvdeq.nx | |
||
frgrncvvdeq.ny | |
||
frgrncvvdeq.x | |
||
frgrncvvdeq.y | |
||
frgrncvvdeq.ne | |
||
frgrncvvdeq.xy | |
||
frgrncvvdeq.f | |
||
frgrncvvdeq.a | |
||
Assertion | frgrncvvdeqlem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frgrncvvdeq.v1 | |
|
2 | frgrncvvdeq.e | |
|
3 | frgrncvvdeq.nx | |
|
4 | frgrncvvdeq.ny | |
|
5 | frgrncvvdeq.x | |
|
6 | frgrncvvdeq.y | |
|
7 | frgrncvvdeq.ne | |
|
8 | frgrncvvdeq.xy | |
|
9 | frgrncvvdeq.f | |
|
10 | frgrncvvdeq.a | |
|
11 | 1 2 3 4 5 6 7 8 9 10 | frgrncvvdeqlem5 | |
12 | fvex | |
|
13 | 12 | snid | |
14 | eleq2 | |
|
15 | 14 | biimpa | |
16 | elin | |
|
17 | 1 2 3 4 5 6 7 8 9 10 | frgrncvvdeqlem1 | |
18 | df-nel | |
|
19 | nelelne | |
|
20 | 18 19 | sylbi | |
21 | 17 20 | syl | |
22 | 21 | adantr | |
23 | 22 | com12 | |
24 | 16 23 | simplbiim | |
25 | 15 24 | syl | |
26 | 13 25 | mpan2 | |
27 | 11 26 | mpcom | |
28 | 27 | ralrimiva | |