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=VtxG
frgrncvvdeq.d D=VtxDegG
frgrwopreglem4a.e E=EdgG
Assertion frgrwopreglem4a GFriendGraphXVYVDXDYXYE

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v V=VtxG
2 frgrncvvdeq.d D=VtxDegG
3 frgrwopreglem4a.e E=EdgG
4 fveq2 X=YDX=DY
5 4 a1i XVYVX=YDX=DY
6 5 necon3d XVYVDXDYXY
7 6 imp XVYVDXDYXY
8 7 3adant1 GFriendGraphXVYVDXDYXY
9 1 2 frgrncvvdeq GFriendGraphxVyVxyGNeighbVtxxDx=Dy
10 oveq2 x=XGNeighbVtxx=GNeighbVtxX
11 neleq2 GNeighbVtxx=GNeighbVtxXyGNeighbVtxxyGNeighbVtxX
12 10 11 syl x=XyGNeighbVtxxyGNeighbVtxX
13 fveqeq2 x=XDx=DyDX=Dy
14 12 13 imbi12d x=XyGNeighbVtxxDx=DyyGNeighbVtxXDX=Dy
15 neleq1 y=YyGNeighbVtxXYGNeighbVtxX
16 fveq2 y=YDy=DY
17 16 eqeq2d y=YDX=DyDX=DY
18 15 17 imbi12d y=YyGNeighbVtxXDX=DyYGNeighbVtxXDX=DY
19 simpll XVYVXYXV
20 sneq x=Xx=X
21 20 difeq2d x=XVx=VX
22 21 adantl XVYVXYx=XVx=VX
23 simpr XVYVYV
24 necom XYYX
25 24 biimpi XYYX
26 23 25 anim12i XVYVXYYVYX
27 eldifsn YVXYVYX
28 26 27 sylibr XVYVXYYVX
29 14 18 19 22 28 rspc2vd XVYVXYxVyVxyGNeighbVtxxDx=DyYGNeighbVtxXDX=DY
30 nnel ¬YGNeighbVtxXYGNeighbVtxX
31 nbgrsym YGNeighbVtxXXGNeighbVtxY
32 frgrusgr GFriendGraphGUSGraph
33 3 nbusgreledg GUSGraphXGNeighbVtxYXYE
34 32 33 syl GFriendGraphXGNeighbVtxYXYE
35 34 biimpd GFriendGraphXGNeighbVtxYXYE
36 31 35 syl5bi GFriendGraphYGNeighbVtxXXYE
37 36 imp GFriendGraphYGNeighbVtxXXYE
38 37 a1d GFriendGraphYGNeighbVtxXDXDYXYE
39 38 expcom YGNeighbVtxXGFriendGraphDXDYXYE
40 39 a1d YGNeighbVtxXXVYVXYGFriendGraphDXDYXYE
41 30 40 sylbi ¬YGNeighbVtxXXVYVXYGFriendGraphDXDYXYE
42 eqneqall DX=DYDXDYXYE
43 42 2a1d DX=DYXVYVXYGFriendGraphDXDYXYE
44 41 43 ja YGNeighbVtxXDX=DYXVYVXYGFriendGraphDXDYXYE
45 44 com12 XVYVXYYGNeighbVtxXDX=DYGFriendGraphDXDYXYE
46 29 45 syld XVYVXYxVyVxyGNeighbVtxxDx=DyGFriendGraphDXDYXYE
47 46 com3l xVyVxyGNeighbVtxxDx=DyGFriendGraphXVYVXYDXDYXYE
48 9 47 mpcom GFriendGraphXVYVXYDXDYXYE
49 48 expd GFriendGraphXVYVXYDXDYXYE
50 49 com34 GFriendGraphXVYVDXDYXYXYE
51 50 3imp GFriendGraphXVYVDXDYXYXYE
52 8 51 mpd GFriendGraphXVYVDXDYXYE