Theorem vdgn0frgrv2

Description: A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

	Ref	Expression
Hypothesis	vdn1frgrv2.v	|- V = ( Vtx ` G )
Assertion	vdgn0frgrv2	|- ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 ) )

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	|- V = ( Vtx ` G )
2		frgrconngr	|- ( G e. FriendGraph -> G e. ConnGraph )
3		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
4		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
5	3 4	syl	|- ( G e. FriendGraph -> G e. UMGraph )
6	1	vdn0conngrumgrv2	|- ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 )
7	6	ex	|- ( ( G e. ConnGraph /\ G e. UMGraph ) -> ( ( N e. V /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 ) )
8	2 5 7	syl2anc	|- ( G e. FriendGraph -> ( ( N e. V /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 ) )
9	8	expdimp	|- ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 ) )