Metamath Proof Explorer

Theorem frgrregorufr0

Description: In a friendship graph there are either no vertices having degree K , or all vertices have degree K for any (nonnegative integer) K , unless there is a universal friend. This corresponds to claim 2 in Huneke p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018) (Revised by AV, 11-May-2021) (Proof shortened by AV, 3-Jan-2022)

Ref Expression
Hypotheses frgrregorufr0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrregorufr0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
frgrregorufr0.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion frgrregorufr0 ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 frgrregorufr0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrregorufr0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 frgrregorufr0.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑦 ) = 𝐾 ) )
5 4 cbvrabv ⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = { 𝑦 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑦 ) = 𝐾 }
6 eqid ⊢ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } )
7 1 3 5 6 frgrwopreg ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 ∨ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ ) ∨ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 ∨ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ∅ ) ) )
8 1 3 5 6 2 frgrwopreg1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
9 8 3mix3d ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
10 9 expcom ⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
11 fveqeq2 ⊢ ( 𝑥 = 𝑣 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑣 ) = 𝐾 ) )
12 11 cbvrabv ⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = { 𝑣 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑣 ) = 𝐾 }
13 12 eqeq1i ⊢ ( { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ ↔ { 𝑣 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑣 ) = 𝐾 } = ∅ )
14 rabeq0 ⊢ ( { 𝑣 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑣 ) = 𝐾 } = ∅ ↔ ∀ 𝑣 ∈ 𝑉 ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 )
15 13 14 bitri ⊢ ( { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ ↔ ∀ 𝑣 ∈ 𝑉 ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 )
16 neqne ⊢ ( ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 )
17 16 ralimi ⊢ ( ∀ 𝑣 ∈ 𝑉 ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 )
18 17 3mix2d ⊢ ( ∀ 𝑣 ∈ 𝑉 ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
19 18 a1d ⊢ ( ∀ 𝑣 ∈ 𝑉 ¬ ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
20 15 19 sylbi ⊢ ( { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
21 10 20 jaoi ⊢ ( ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 ∨ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ ) → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
22 1 3 5 6 2 frgrwopreg2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
23 22 3mix3d ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
24 23 expcom ⊢ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
25 difrab0eq ⊢ ( ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ∅ ↔ 𝑉 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } )
26 12 eqeq2i ⊢ ( 𝑉 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ↔ 𝑉 = { 𝑣 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑣 ) = 𝐾 } )
27 rabid2 ⊢ ( 𝑉 = { 𝑣 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑣 ) = 𝐾 } ↔ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 )
28 26 27 bitri ⊢ ( 𝑉 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ↔ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 )
29 3mix1 ⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
30 29 a1d ⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
31 28 30 sylbi ⊢ ( 𝑉 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
32 25 31 sylbi ⊢ ( ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ∅ → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
33 24 32 jaoi ⊢ ( ( ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 ∨ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ∅ ) → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
34 21 33 jaoi ⊢ ( ( ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = 1 ∨ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } = ∅ ) ∨ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) ) = 1 ∨ ( 𝑉 ∖ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ) = ∅ ) ) → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
35 7 34 mpcom ⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )