Theorem frgrregorufr

Description: If there is a vertex having degree K for each (nonnegative integer) K in a friendship graph, then either all vertices have degree K or there is a universal friend. This corresponds to claim 2 in Huneke p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018)

	Ref	Expression
Hypotheses	frgrregorufr0.v	|- V = ( Vtx ` G )
	frgrregorufr0.e	|- E = ( Edg ` G )
	frgrregorufr0.d	|- D = ( VtxDeg ` G )
Assertion	frgrregorufr	|- ( G e. FriendGraph -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrregorufr0.v	|- V = ( Vtx ` G )
2		frgrregorufr0.e	|- E = ( Edg ` G )
3		frgrregorufr0.d	|- D = ( VtxDeg ` G )
4	1 2 3	frgrregorufr0	|- ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
5		orc	|- ( A. v e. V ( D ` v ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
6	5	a1d	|- ( A. v e. V ( D ` v ) = K -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
7		fveq2	|- ( v = a -> ( D ` v ) = ( D ` a ) )
8	7	neeq1d	|- ( v = a -> ( ( D ` v ) =/= K <-> ( D ` a ) =/= K ) )
9	8	rspcva	|- ( ( a e. V /\ A. v e. V ( D ` v ) =/= K ) -> ( D ` a ) =/= K )
10		df-ne	|- ( ( D ` a ) =/= K <-> -. ( D ` a ) = K )
11		pm2.21	|- ( -. ( D ` a ) = K -> ( ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
12	10 11	sylbi	|- ( ( D ` a ) =/= K -> ( ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
13	9 12	syl	|- ( ( a e. V /\ A. v e. V ( D ` v ) =/= K ) -> ( ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
14	13	ancoms	|- ( ( A. v e. V ( D ` v ) =/= K /\ a e. V ) -> ( ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
15	14	rexlimdva	|- ( A. v e. V ( D ` v ) =/= K -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
16		olc	|- ( E. v e. V A. w e. ( V \ { v } ) { v , w } e. E -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
17	16	a1d	|- ( E. v e. V A. w e. ( V \ { v } ) { v , w } e. E -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
18	6 15 17	3jaoi	|- ( ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
19	4 18	syl	|- ( G e. FriendGraph -> ( E. a e. V ( D ` a ) = K -> ( A. v e. V ( D ` v ) = K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )