Theorem frgrconngr

Description: A friendship graph is connected, see remark 1 in MertziosUnger p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 1-Apr-2021)

	Ref	Expression
Assertion	frgrconngr	|- ( G e. FriendGraph -> G e. ConnGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2	1	2pthfrgr	|- ( G e. FriendGraph -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p ( f ( k ( SPathsOn ` G ) n ) p /\ ( # ` f ) = 2 ) )
3		spthonpthon	|- ( f ( k ( SPathsOn ` G ) n ) p -> f ( k ( PathsOn ` G ) n ) p )
4	3	adantr	|- ( ( f ( k ( SPathsOn ` G ) n ) p /\ ( # ` f ) = 2 ) -> f ( k ( PathsOn ` G ) n ) p )
5	4	2eximi	|- ( E. f E. p ( f ( k ( SPathsOn ` G ) n ) p /\ ( # ` f ) = 2 ) -> E. f E. p f ( k ( PathsOn ` G ) n ) p )
6	5	2ralimi	|- ( A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p ( f ( k ( SPathsOn ` G ) n ) p /\ ( # ` f ) = 2 ) -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
7	2 6	syl	|- ( G e. FriendGraph -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
8	1	isconngr1	|- ( G e. FriendGraph -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
9	7 8	mpbird	|- ( G e. FriendGraph -> G e. ConnGraph )