frgrwopreglem2

Description: Lemma 2 for frgrwopreg . If the set A of vertices of degree K is not empty in a friendship graph with at least two vertices, then K must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 2-Jan-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 )
Assertion	frgrwopreglem2	\|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) /\ A =/= (/) ) -> 2 <_ K )

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		n0	\|- ( A =/= (/) <-> E. x x e. A )
6	3	reqabi	\|- ( x e. A <-> ( x e. V /\ ( D ` x ) = K ) )
7	1	vdgfrgrgt2	\|- ( ( G e. FriendGraph /\ x e. V ) -> ( 1 < ( # ` V ) -> 2 <_ ( ( VtxDeg ` G ) ` x ) ) )
8	7	imp	\|- ( ( ( G e. FriendGraph /\ x e. V ) /\ 1 < ( # ` V ) ) -> 2 <_ ( ( VtxDeg ` G ) ` x ) )
9		breq2	\|- ( K = ( D ` x ) -> ( 2 <_ K <-> 2 <_ ( D ` x ) ) )
10	2	fveq1i	\|- ( D ` x ) = ( ( VtxDeg ` G ) ` x )
11	10	breq2i	\|- ( 2 <_ ( D ` x ) <-> 2 <_ ( ( VtxDeg ` G ) ` x ) )
12	9 11	bitrdi	\|- ( K = ( D ` x ) -> ( 2 <_ K <-> 2 <_ ( ( VtxDeg ` G ) ` x ) ) )
13	12	eqcoms	\|- ( ( D ` x ) = K -> ( 2 <_ K <-> 2 <_ ( ( VtxDeg ` G ) ` x ) ) )
14	8 13	syl5ibrcom	\|- ( ( ( G e. FriendGraph /\ x e. V ) /\ 1 < ( # ` V ) ) -> ( ( D ` x ) = K -> 2 <_ K ) )
15	14	exp31	\|- ( G e. FriendGraph -> ( x e. V -> ( 1 < ( # ` V ) -> ( ( D ` x ) = K -> 2 <_ K ) ) ) )
16	15	com14	\|- ( ( D ` x ) = K -> ( x e. V -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) )
17	16	impcom	\|- ( ( x e. V /\ ( D ` x ) = K ) -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) )
18	6 17	sylbi	\|- ( x e. A -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) )
19	18	exlimiv	\|- ( E. x x e. A -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) )
20	5 19	sylbi	\|- ( A =/= (/) -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) )
21	20	3imp31	\|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) /\ A =/= (/) ) -> 2 <_ K )

Metamath Proof Explorer

Theorem frgrwopreglem2

Proof