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 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) )