Theorem 3cyclfrgrrn

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

	Ref	Expression
Hypotheses	3cyclfrgrrn1.v	|- V = ( Vtx ` G )
	3cyclfrgrrn1.e	|- E = ( Edg ` G )
Assertion	3cyclfrgrrn	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		3cyclfrgrrn1.v	|- V = ( Vtx ` G )
2		3cyclfrgrrn1.e	|- E = ( Edg ` G )
3	1	fvexi	|- V e. _V
4		hashgt12el2	|- ( ( V e. _V /\ 1 < ( # ` V ) /\ a e. V ) -> E. x e. V a =/= x )
5	3 4	mp3an1	|- ( ( 1 < ( # ` V ) /\ a e. V ) -> E. x e. V a =/= x )
6		simpr	|- ( ( ( x e. V /\ a =/= x /\ a e. V ) /\ G e. FriendGraph ) -> G e. FriendGraph )
7		pm3.22	|- ( ( x e. V /\ a e. V ) -> ( a e. V /\ x e. V ) )
8	7	3adant2	|- ( ( x e. V /\ a =/= x /\ a e. V ) -> ( a e. V /\ x e. V ) )
9	8	adantr	|- ( ( ( x e. V /\ a =/= x /\ a e. V ) /\ G e. FriendGraph ) -> ( a e. V /\ x e. V ) )
10		simpl2	|- ( ( ( x e. V /\ a =/= x /\ a e. V ) /\ G e. FriendGraph ) -> a =/= x )
11	1 2	3cyclfrgrrn1	|- ( ( G e. FriendGraph /\ ( a e. V /\ x e. V ) /\ a =/= x ) -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
12	6 9 10 11	syl3anc	|- ( ( ( x e. V /\ a =/= x /\ a e. V ) /\ G e. FriendGraph ) -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
13	12	3exp1	|- ( x e. V -> ( a =/= x -> ( a e. V -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) ) )
14	13	rexlimiv	|- ( E. x e. V a =/= x -> ( a e. V -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
15	5 14	syl	|- ( ( 1 < ( # ` V ) /\ a e. V ) -> ( a e. V -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
16	15	expcom	|- ( a e. V -> ( 1 < ( # ` V ) -> ( a e. V -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) ) )
17	16	pm2.43a	|- ( a e. V -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
18	17	com13	|- ( G e. FriendGraph -> ( 1 < ( # ` V ) -> ( a e. V -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
19	18	imp	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( a e. V -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )
20	19	ralrimiv	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )