Description: In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 4-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frgrncvvdeq.v | |
|
frgrncvvdeq.d | |
||
frgrwopreglem4a.e | |
||
Assertion | frgrwopreglem4a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frgrncvvdeq.v | |
|
2 | frgrncvvdeq.d | |
|
3 | frgrwopreglem4a.e | |
|
4 | fveq2 | |
|
5 | 4 | a1i | |
6 | 5 | necon3d | |
7 | 6 | imp | |
8 | 7 | 3adant1 | |
9 | 1 2 | frgrncvvdeq | |
10 | oveq2 | |
|
11 | neleq2 | |
|
12 | 10 11 | syl | |
13 | fveqeq2 | |
|
14 | 12 13 | imbi12d | |
15 | neleq1 | |
|
16 | fveq2 | |
|
17 | 16 | eqeq2d | |
18 | 15 17 | imbi12d | |
19 | simpll | |
|
20 | sneq | |
|
21 | 20 | difeq2d | |
22 | 21 | adantl | |
23 | simpr | |
|
24 | necom | |
|
25 | 24 | biimpi | |
26 | 23 25 | anim12i | |
27 | eldifsn | |
|
28 | 26 27 | sylibr | |
29 | 14 18 19 22 28 | rspc2vd | |
30 | nnel | |
|
31 | nbgrsym | |
|
32 | frgrusgr | |
|
33 | 3 | nbusgreledg | |
34 | 32 33 | syl | |
35 | 34 | biimpd | |
36 | 31 35 | syl5bi | |
37 | 36 | imp | |
38 | 37 | a1d | |
39 | 38 | expcom | |
40 | 39 | a1d | |
41 | 30 40 | sylbi | |
42 | eqneqall | |
|
43 | 42 | 2a1d | |
44 | 41 43 | ja | |
45 | 44 | com12 | |
46 | 29 45 | syld | |
47 | 46 | com3l | |
48 | 9 47 | mpcom | |
49 | 48 | expd | |
50 | 49 | com34 | |
51 | 50 | 3imp | |
52 | 8 51 | mpd | |