# Metamath Proof Explorer

## Theorem frgrwopreglem4a

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 ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
frgrncvvdeq.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
frgrwopreglem4a.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion frgrwopreglem4a ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {D}\left({X}\right)\ne {D}\left({Y}\right)\right)\to \left\{{X},{Y}\right\}\in {E}$

### Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frgrncvvdeq.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
3 frgrwopreglem4a.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
4 fveq2 ${⊢}{X}={Y}\to {D}\left({X}\right)={D}\left({Y}\right)$
5 4 a1i ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({X}={Y}\to {D}\left({X}\right)={D}\left({Y}\right)\right)$
6 5 necon3d ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to {X}\ne {Y}\right)$
7 6 imp ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {D}\left({X}\right)\ne {D}\left({Y}\right)\right)\to {X}\ne {Y}$
8 7 3adant1 ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {D}\left({X}\right)\ne {D}\left({Y}\right)\right)\to {X}\ne {Y}$
9 1 2 frgrncvvdeq ${⊢}{G}\in \mathrm{FriendGraph}\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({V}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)\to {D}\left({x}\right)={D}\left({y}\right)\right)$
10 oveq2 ${⊢}{x}={X}\to {G}\mathrm{NeighbVtx}{x}={G}\mathrm{NeighbVtx}{X}$
11 neleq2 ${⊢}{G}\mathrm{NeighbVtx}{x}={G}\mathrm{NeighbVtx}{X}\to \left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)↔{y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\right)$
12 10 11 syl ${⊢}{x}={X}\to \left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)↔{y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\right)$
13 fveqeq2 ${⊢}{x}={X}\to \left({D}\left({x}\right)={D}\left({y}\right)↔{D}\left({X}\right)={D}\left({y}\right)\right)$
14 12 13 imbi12d ${⊢}{x}={X}\to \left(\left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)\to {D}\left({x}\right)={D}\left({y}\right)\right)↔\left({y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({y}\right)\right)\right)$
15 neleq1 ${⊢}{y}={Y}\to \left({y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)↔{Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\right)$
16 fveq2 ${⊢}{y}={Y}\to {D}\left({y}\right)={D}\left({Y}\right)$
17 16 eqeq2d ${⊢}{y}={Y}\to \left({D}\left({X}\right)={D}\left({y}\right)↔{D}\left({X}\right)={D}\left({Y}\right)\right)$
18 15 17 imbi12d ${⊢}{y}={Y}\to \left(\left({y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({y}\right)\right)↔\left({Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({Y}\right)\right)\right)$
19 simpll ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to {X}\in {V}$
20 sneq ${⊢}{x}={X}\to \left\{{x}\right\}=\left\{{X}\right\}$
21 20 difeq2d ${⊢}{x}={X}\to {V}\setminus \left\{{x}\right\}={V}\setminus \left\{{X}\right\}$
22 21 adantl ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\wedge {x}={X}\right)\to {V}\setminus \left\{{x}\right\}={V}\setminus \left\{{X}\right\}$
23 simpr ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to {Y}\in {V}$
24 necom ${⊢}{X}\ne {Y}↔{Y}\ne {X}$
25 24 biimpi ${⊢}{X}\ne {Y}\to {Y}\ne {X}$
26 23 25 anim12i ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({Y}\in {V}\wedge {Y}\ne {X}\right)$
27 eldifsn ${⊢}{Y}\in \left({V}\setminus \left\{{X}\right\}\right)↔\left({Y}\in {V}\wedge {Y}\ne {X}\right)$
28 26 27 sylibr ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to {Y}\in \left({V}\setminus \left\{{X}\right\}\right)$
29 14 18 19 22 28 rspc2vd ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left(\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({V}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)\to {D}\left({x}\right)={D}\left({y}\right)\right)\to \left({Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({Y}\right)\right)\right)$
30 nnel ${⊢}¬{Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)↔{Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)$
31 nbgrsym ${⊢}{Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)↔{X}\in \left({G}\mathrm{NeighbVtx}{Y}\right)$
32 frgrusgr ${⊢}{G}\in \mathrm{FriendGraph}\to {G}\in \mathrm{USGraph}$
33 3 nbusgreledg ${⊢}{G}\in \mathrm{USGraph}\to \left({X}\in \left({G}\mathrm{NeighbVtx}{Y}\right)↔\left\{{X},{Y}\right\}\in {E}\right)$
34 32 33 syl ${⊢}{G}\in \mathrm{FriendGraph}\to \left({X}\in \left({G}\mathrm{NeighbVtx}{Y}\right)↔\left\{{X},{Y}\right\}\in {E}\right)$
35 34 biimpd ${⊢}{G}\in \mathrm{FriendGraph}\to \left({X}\in \left({G}\mathrm{NeighbVtx}{Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)$
36 31 35 syl5bi ${⊢}{G}\in \mathrm{FriendGraph}\to \left({Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)\to \left\{{X},{Y}\right\}\in {E}\right)$
37 36 imp ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)\right)\to \left\{{X},{Y}\right\}\in {E}$
38 37 a1d ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)$
39 38 expcom ${⊢}{Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)$
40 39 a1d ${⊢}{Y}\in \left({G}\mathrm{NeighbVtx}{X}\right)\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
41 30 40 sylbi ${⊢}¬{Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
42 eqneqall ${⊢}{D}\left({X}\right)={D}\left({Y}\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)$
43 42 2a1d ${⊢}{D}\left({X}\right)={D}\left({Y}\right)\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
44 41 43 ja ${⊢}\left({Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({Y}\right)\right)\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
45 44 com12 ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left(\left({Y}\notin \left({G}\mathrm{NeighbVtx}{X}\right)\to {D}\left({X}\right)={D}\left({Y}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
46 29 45 syld ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left(\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({V}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)\to {D}\left({x}\right)={D}\left({y}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
47 46 com3l ${⊢}\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({V}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({y}\notin \left({G}\mathrm{NeighbVtx}{x}\right)\to {D}\left({x}\right)={D}\left({y}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
48 9 47 mpcom ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left(\left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {X}\ne {Y}\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)$
49 48 expd ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({X}\ne {Y}\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
50 49 com34 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({D}\left({X}\right)\ne {D}\left({Y}\right)\to \left({X}\ne {Y}\to \left\{{X},{Y}\right\}\in {E}\right)\right)\right)$
51 50 3imp ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {D}\left({X}\right)\ne {D}\left({Y}\right)\right)\to \left({X}\ne {Y}\to \left\{{X},{Y}\right\}\in {E}\right)$
52 8 51 mpd ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {D}\left({X}\right)\ne {D}\left({Y}\right)\right)\to \left\{{X},{Y}\right\}\in {E}$