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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
	frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
	frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
	frgrwopreg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frgrwopreglem4	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3		frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4		frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5		frgrwopreg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
6		simpl	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐺 ∈ FriendGraph )
7		elrabi	⊢ ( 𝑎 ∈ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } → 𝑎 ∈ 𝑉 )
8	7 3	eleq2s	⊢ ( 𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉 )
9		eldifi	⊢ ( 𝑏 ∈ ( 𝑉 ∖ 𝐴 ) → 𝑏 ∈ 𝑉 )
10	9 4	eleq2s	⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉 )
11	8 10	anim12i	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
12	11	adantl	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
13	1 2 3 4	frgrwopreglem3	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) )
14	13	adantl	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) )
15	1 2 5	frgrwopreglem4a	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
16	6 12 14 15	syl3anc	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
17	16	ralrimivva	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 )