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 e. V | ( D ` x ) = K }
	frgrwopreg.b	|- B = ( V \ A )
	frgrwopreg.e	|- E = ( Edg ` G )
Assertion	frgrwopreglem4	|- ( G e. FriendGraph -> A. a e. A A. b e. B { a , b } e. E )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	|- V = ( Vtx ` G )
2		frgrwopreg.d	|- D = ( VtxDeg ` G )
3		frgrwopreg.a	|- A = { x e. V | ( D ` x ) = K }
4		frgrwopreg.b	|- B = ( V \ A )
5		frgrwopreg.e	|- E = ( Edg ` G )
6		simpl	|- ( ( G e. FriendGraph /\ ( a e. A /\ b e. B ) ) -> G e. FriendGraph )
7		elrabi	|- ( a e. { x e. V | ( D ` x ) = K } -> a e. V )
8	7 3	eleq2s	|- ( a e. A -> a e. V )
9		eldifi	|- ( b e. ( V \ A ) -> b e. V )
10	9 4	eleq2s	|- ( b e. B -> b e. V )
11	8 10	anim12i	|- ( ( a e. A /\ b e. B ) -> ( a e. V /\ b e. V ) )
12	11	adantl	|- ( ( G e. FriendGraph /\ ( a e. A /\ b e. B ) ) -> ( a e. V /\ b e. V ) )
13	1 2 3 4	frgrwopreglem3	|- ( ( a e. A /\ b e. B ) -> ( D ` a ) =/= ( D ` b ) )
14	13	adantl	|- ( ( G e. FriendGraph /\ ( a e. A /\ b e. B ) ) -> ( D ` a ) =/= ( D ` b ) )
15	1 2 5	frgrwopreglem4a	|- ( ( G e. FriendGraph /\ ( a e. V /\ b e. V ) /\ ( D ` a ) =/= ( D ` b ) ) -> { a , b } e. E )
16	6 12 14 15	syl3anc	|- ( ( G e. FriendGraph /\ ( a e. A /\ b e. B ) ) -> { a , b } e. E )
17	16	ralrimivva	|- ( G e. FriendGraph -> A. a e. A A. b e. B { a , b } e. E )