Theorem vdgn1frgrv3

Description: Any vertex in a friendship graph does not have degree 1, see remark 2 in MertziosUnger p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018) (Revised by AV, 4-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	|- V = ( Vtx ` G )
2	1	vdgn1frgrv2	|- ( ( G e. FriendGraph /\ v e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` v ) =/= 1 ) )
3	2	impancom	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( v e. V -> ( ( VtxDeg ` G ) ` v ) =/= 1 ) )
4	3	ralrimiv	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 )