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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrregorufr0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	frgrregorufr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	frgrregorufr	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrregorufr0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrregorufr0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		frgrregorufr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4	1 2 3	frgrregorufr0	⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
5		orc	⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
6	5	a1d	⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
7		fveq2	⊢ ( 𝑣 = 𝑎 → ( 𝐷 ‘ 𝑣 ) = ( 𝐷 ‘ 𝑎 ) )
8	7	neeq1d	⊢ ( 𝑣 = 𝑎 → ( ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ↔ ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 ) )
9	8	rspcva	⊢ ( ( 𝑎 ∈ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ) → ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 )
10		df-ne	⊢ ( ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 ↔ ¬ ( 𝐷 ‘ 𝑎 ) = 𝐾 )
11		pm2.21	⊢ ( ¬ ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
12	10 11	sylbi	⊢ ( ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
13	9 12	syl	⊢ ( ( 𝑎 ∈ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ) → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
14	13	ancoms	⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
15	14	rexlimdva	⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
16		olc	⊢ ( ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
17	16	a1d	⊢ ( ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
18	6 15 17	3jaoi	⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
19	4 18	syl	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )