Theorem 3cyclfrgrrn2

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

	Ref	Expression
Hypotheses	3cyclfrgrrn1.v	|- V = ( Vtx ` G )
	3cyclfrgrrn1.e	|- E = ( Edg ` G )
Assertion	3cyclfrgrrn2	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { 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 2	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 ) )
4		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
5	2	usgredgne	|- ( ( G e. USGraph /\ { b , c } e. E ) -> b =/= c )
6	5	expcom	|- ( { b , c } e. E -> ( G e. USGraph -> b =/= c ) )
7	6	3ad2ant2	|- ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> ( G e. USGraph -> b =/= c ) )
8	4 7	syl5com	|- ( G e. FriendGraph -> ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> b =/= c ) )
9	8	adantr	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> b =/= c ) )
10	9	ancrd	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> ( b =/= c /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
11	10	reximdv	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> E. c e. V ( b =/= c /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
12	11	reximdv	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
13	12	ralimdv	|- ( ( 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 ) -> A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) ) )
14	3 13	mpd	|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )