Metamath Proof Explorer

Theorem frgrwopreglem4

Description: Lemma 4 for frgrwopreg . In a friendship graph each vertex with degree K is connected with any vertex with degree other than K . This corresponds to statement 4 in Huneke p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B.". (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 4-Feb-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢ V = Vtx ⁡ G
frgrwopreg.d ⊢ D = VtxDeg ⁡ G
frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
frgrwopreg.b ⊢ B = V ∖ A
frgrwopreg.e ⊢ E = Edg ⁡ G
Assertion frgrwopreglem4 ⊢ G ∈ FriendGraph → ∀ a ∈ A ∀ b ∈ B a b ∈ E

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ V = Vtx ⁡ G
2 frgrwopreg.d ⊢ D = VtxDeg ⁡ G
3 frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
4 frgrwopreg.b ⊢ B = V ∖ A
5 frgrwopreg.e ⊢ E = Edg ⁡ G
6 simpl ⊢ G ∈ FriendGraph ∧ a ∈ A ∧ b ∈ B → G ∈ FriendGraph
7 elrabi ⊢ a ∈ x ∈ V | D ⁡ x = K → a ∈ V
8 7 3 eleq2s ⊢ a ∈ A → a ∈ V
9 eldifi ⊢ b ∈ V ∖ A → b ∈ V
10 9 4 eleq2s ⊢ b ∈ B → b ∈ V
11 8 10 anim12i ⊢ a ∈ A ∧ b ∈ B → a ∈ V ∧ b ∈ V
12 11 adantl ⊢ G ∈ FriendGraph ∧ a ∈ A ∧ b ∈ B → a ∈ V ∧ b ∈ V
13 1 2 3 4 frgrwopreglem3 ⊢ a ∈ A ∧ b ∈ B → D ⁡ a ≠ D ⁡ b
14 13 adantl ⊢ G ∈ FriendGraph ∧ a ∈ A ∧ b ∈ B → D ⁡ a ≠ D ⁡ b
15 1 2 5 frgrwopreglem4a ⊢ G ∈ FriendGraph ∧ a ∈ V ∧ b ∈ V ∧ D ⁡ a ≠ D ⁡ b → a b ∈ E
16 6 12 14 15 syl3anc ⊢ G ∈ FriendGraph ∧ a ∈ A ∧ b ∈ B → a b ∈ E
17 16 ralrimivva ⊢ G ∈ FriendGraph → ∀ a ∈ A ∀ b ∈ B a b ∈ E