Theorem 3cyclfrgr

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

	Ref	Expression
Hypothesis	3cyclfrgr.v	|- V = ( Vtx ` G )
Assertion	3cyclfrgr	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) )

Proof

Step	Hyp	Ref	Expression
1		3cyclfrgr.v	|- V = ( Vtx ` G )
2		eqid	|- ( Edg ` G ) = ( Edg ` G )
3	1 2	3cyclfrgrrn	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V E. b e. V E. c e. V ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) )
4		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
5		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
6	4 5	syl	|- ( G e. FriendGraph -> G e. UMGraph )
7	6	ad4antr	|- ( ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) ) -> G e. UMGraph )
8		simpr	|- ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) -> v e. V )
9	8	anim1i	|- ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) -> ( v e. V /\ ( b e. V /\ c e. V ) ) )
10		3anass	|- ( ( v e. V /\ b e. V /\ c e. V ) <-> ( v e. V /\ ( b e. V /\ c e. V ) ) )
11	9 10	sylibr	|- ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) -> ( v e. V /\ b e. V /\ c e. V ) )
12	11	adantr	|- ( ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) ) -> ( v e. V /\ b e. V /\ c e. V ) )
13		simpr	|- ( ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) ) -> ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) )
14	1 2	umgr3cyclex	|- ( ( G e. UMGraph /\ ( v e. V /\ b e. V /\ c e. V ) /\ ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) )
15	7 12 13 14	syl3anc	|- ( ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) )
16	15	ex	|- ( ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) ) )
17	16	rexlimdvva	|- ( ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) /\ v e. V ) -> ( E. b e. V E. c e. V ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) ) )
18	17	ralimdva	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( A. v e. V E. b e. V E. c e. V ( { v , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , v } e. ( Edg ` G ) ) -> A. v e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) ) )
19	3 18	mpd	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = v ) )