Metamath Proof Explorer


Theorem frgrncvvdeq

Description: In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in Huneke p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 10-May-2021)

Ref Expression
Hypotheses frgrncvvdeq.v 𝑉 = ( Vtx ‘ 𝐺 )
frgrncvvdeq.d 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion frgrncvvdeq ( 𝐺 ∈ FriendGraph → ∀ 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷𝑥 ) = ( 𝐷𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrncvvdeq.d 𝐷 = ( VtxDeg ‘ 𝐺 )
3 ovexd ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 NeighbVtx 𝑥 ) ∈ V )
4 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
5 eqid ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝑥 )
6 eqid ( 𝐺 NeighbVtx 𝑦 ) = ( 𝐺 NeighbVtx 𝑦 )
7 simpl ( ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑥𝑉 )
8 7 ad2antlr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑥𝑉 )
9 eldifi ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) → 𝑦𝑉 )
10 9 adantl ( ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑦𝑉 )
11 10 ad2antlr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑦𝑉 )
12 eldif ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑦𝑉 ∧ ¬ 𝑦 ∈ { 𝑥 } ) )
13 velsn ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
14 13 biimpri ( 𝑦 = 𝑥𝑦 ∈ { 𝑥 } )
15 14 equcoms ( 𝑥 = 𝑦𝑦 ∈ { 𝑥 } )
16 15 necon3bi ( ¬ 𝑦 ∈ { 𝑥 } → 𝑥𝑦 )
17 12 16 simplbiim ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) → 𝑥𝑦 )
18 17 adantl ( ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑥𝑦 )
19 18 ad2antlr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑥𝑦 )
20 simpr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) )
21 simpl ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → 𝐺 ∈ FriendGraph )
22 21 adantr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝐺 ∈ FriendGraph )
23 eqid ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) = ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
24 1 4 5 6 8 11 19 20 22 23 frgrncvvdeqlem10 ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) : ( 𝐺 NeighbVtx 𝑥 ) –1-1-onto→ ( 𝐺 NeighbVtx 𝑦 ) )
25 3 24 hasheqf1od ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) )
26 frgrusgr ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
27 26 7 anim12i ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝑥𝑉 ) )
28 27 adantr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑥𝑉 ) )
29 1 hashnbusgrvd ( ( 𝐺 ∈ USGraph ∧ 𝑥𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
30 28 29 syl ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
31 26 10 anim12i ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝑦𝑉 ) )
32 31 adantr ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑦𝑉 ) )
33 1 hashnbusgrvd ( ( 𝐺 ∈ USGraph ∧ 𝑦𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) )
34 32 33 syl ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) )
35 25 30 34 3eqtr3d ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) )
36 2 fveq1i ( 𝐷𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 )
37 2 fveq1i ( 𝐷𝑦 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 )
38 35 36 37 3eqtr4g ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐷𝑥 ) = ( 𝐷𝑦 ) )
39 38 ex ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷𝑥 ) = ( 𝐷𝑦 ) ) )
40 39 ralrimivva ( 𝐺 ∈ FriendGraph → ∀ 𝑥𝑉𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷𝑥 ) = ( 𝐷𝑦 ) ) )