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 
|- V = ( Vtx ` G )
frgrncvvdeq.d 
|- D = ( VtxDeg ` G )
Assertion frgrncvvdeq 
|- ( G e. FriendGraph -> A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v 
 |-  V = ( Vtx ` G )
2 frgrncvvdeq.d 
 |-  D = ( VtxDeg ` G )
3 ovexd 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( G NeighbVtx x ) e. _V )
4 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
5 eqid 
 |-  ( G NeighbVtx x ) = ( G NeighbVtx x )
6 eqid 
 |-  ( G NeighbVtx y ) = ( G NeighbVtx y )
7 simpl 
 |-  ( ( x e. V /\ y e. ( V \ { x } ) ) -> x e. V )
8 7 ad2antlr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> x e. V )
9 eldifi 
 |-  ( y e. ( V \ { x } ) -> y e. V )
10 9 adantl 
 |-  ( ( x e. V /\ y e. ( V \ { x } ) ) -> y e. V )
11 10 ad2antlr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> y e. V )
12 eldif 
 |-  ( y e. ( V \ { x } ) <-> ( y e. V /\ -. y e. { x } ) )
13 velsn 
 |-  ( y e. { x } <-> y = x )
14 13 biimpri 
 |-  ( y = x -> y e. { x } )
15 14 equcoms 
 |-  ( x = y -> y e. { x } )
16 15 necon3bi 
 |-  ( -. y e. { x } -> x =/= y )
17 12 16 simplbiim 
 |-  ( y e. ( V \ { x } ) -> x =/= y )
18 17 adantl 
 |-  ( ( x e. V /\ y e. ( V \ { x } ) ) -> x =/= y )
19 18 ad2antlr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> x =/= y )
20 simpr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> y e/ ( G NeighbVtx x ) )
21 simpl 
 |-  ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) -> G e. FriendGraph )
22 21 adantr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> G e. FriendGraph )
23 eqid 
 |-  ( a e. ( G NeighbVtx x ) |-> ( iota_ b e. ( G NeighbVtx y ) { a , b } e. ( Edg ` G ) ) ) = ( a e. ( G NeighbVtx x ) |-> ( iota_ b e. ( G NeighbVtx y ) { a , b } e. ( Edg ` G ) ) )
24 1 4 5 6 8 11 19 20 22 23 frgrncvvdeqlem10 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( a e. ( G NeighbVtx x ) |-> ( iota_ b e. ( G NeighbVtx y ) { a , b } e. ( Edg ` G ) ) ) : ( G NeighbVtx x ) -1-1-onto-> ( G NeighbVtx y ) )
25 3 24 hasheqf1od 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( # ` ( G NeighbVtx x ) ) = ( # ` ( G NeighbVtx y ) ) )
26 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
27 26 7 anim12i 
 |-  ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) -> ( G e. USGraph /\ x e. V ) )
28 27 adantr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( G e. USGraph /\ x e. V ) )
29 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ x e. V ) -> ( # ` ( G NeighbVtx x ) ) = ( ( VtxDeg ` G ) ` x ) )
30 28 29 syl 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( # ` ( G NeighbVtx x ) ) = ( ( VtxDeg ` G ) ` x ) )
31 26 10 anim12i 
 |-  ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) -> ( G e. USGraph /\ y e. V ) )
32 31 adantr 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( G e. USGraph /\ y e. V ) )
33 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ y e. V ) -> ( # ` ( G NeighbVtx y ) ) = ( ( VtxDeg ` G ) ` y ) )
34 32 33 syl 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( # ` ( G NeighbVtx y ) ) = ( ( VtxDeg ` G ) ` y ) )
35 25 30 34 3eqtr3d 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( ( VtxDeg ` G ) ` x ) = ( ( VtxDeg ` G ) ` y ) )
36 2 fveq1i 
 |-  ( D ` x ) = ( ( VtxDeg ` G ) ` x )
37 2 fveq1i 
 |-  ( D ` y ) = ( ( VtxDeg ` G ) ` y )
38 35 36 37 3eqtr4g 
 |-  ( ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) /\ y e/ ( G NeighbVtx x ) ) -> ( D ` x ) = ( D ` y ) )
39 38 ex 
 |-  ( ( G e. FriendGraph /\ ( x e. V /\ y e. ( V \ { x } ) ) ) -> ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) )
40 39 ralrimivva 
 |-  ( G e. FriendGraph -> A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) )