Metamath Proof Explorer


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 → ( ∃ 𝑎𝑉 ( 𝐷𝑎 ) = 𝐾 → ( ∀ 𝑣𝑉 ( 𝐷𝑣 ) = 𝐾 ∨ ∃ 𝑣𝑉𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )