Theorem frgrregorufrg

Description: If there is a vertex having degree k for each nonnegative integer k in a friendship graph, then 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". Variant of frgrregorufr with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Revised by AV, 26-May-2021) (Proof shortened by AV, 12-Jan-2022)

	Ref	Expression
Hypotheses	frgrregorufrg.v	|- V = ( Vtx ` G )
	frgrregorufrg.e	|- E = ( Edg ` G )
Assertion	frgrregorufrg	|- ( G e. FriendGraph -> A. k e. NN0 ( E. a e. V ( ( VtxDeg ` G ) ` a ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrregorufrg.v	|- V = ( Vtx ` G )
2		frgrregorufrg.e	|- E = ( Edg ` G )
3		eqid	|- ( VtxDeg ` G ) = ( VtxDeg ` G )
4	1 2 3	frgrregorufr	|- ( G e. FriendGraph -> ( E. a e. V ( ( VtxDeg ` G ) ` a ) = k -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
5	4	adantr	|- ( ( G e. FriendGraph /\ k e. NN0 ) -> ( E. a e. V ( ( VtxDeg ` G ) ` a ) = k -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
6		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
7		nn0xnn0	|- ( k e. NN0 -> k e. NN0* )
8	1 3	usgreqdrusgr	|- ( ( G e. USGraph /\ k e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = k ) -> G RegUSGraph k )
9	8	3expia	|- ( ( G e. USGraph /\ k e. NN0* ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = k -> G RegUSGraph k ) )
10	6 7 9	syl2an	|- ( ( G e. FriendGraph /\ k e. NN0 ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = k -> G RegUSGraph k ) )
11	10	orim1d	|- ( ( G e. FriendGraph /\ k e. NN0 ) -> ( ( A. v e. V ( ( VtxDeg ` G ) ` v ) = k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
12	5 11	syld	|- ( ( G e. FriendGraph /\ k e. NN0 ) -> ( E. a e. V ( ( VtxDeg ` G ) ` a ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
13	12	ralrimiva	|- ( G e. FriendGraph -> A. k e. NN0 ( E. a e. V ( ( VtxDeg ` G ) ` a ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )