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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrregorufrg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frgrregorufrg	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑎 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑎 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrregorufrg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrregorufrg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
4	1 2 3	frgrregorufr	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑎 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑎 ) = 𝑘 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
5	4	adantr	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑘 ∈ ℕ0 ) → ( ∃ 𝑎 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑎 ) = 𝑘 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
6		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
7		nn0xnn0	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0* )
8	1 3	usgreqdrusgr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ) → 𝐺 RegUSGraph 𝑘 )
9	8	3expia	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑘 ∈ ℕ0* ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 → 𝐺 RegUSGraph 𝑘 ) )
10	6 7 9	syl2an	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑘 ∈ ℕ0 ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 → 𝐺 RegUSGraph 𝑘 ) )
11	10	orim1d	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑘 ∈ ℕ0 ) → ( ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
12	5 11	syld	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑘 ∈ ℕ0 ) → ( ∃ 𝑎 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑎 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
13	12	ralrimiva	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑎 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑎 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )