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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	3cyclfrgr	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		3cyclfrgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3	1 2	3cyclfrgrrn	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
4		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
5		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
6	4 5	syl	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UMGraph )
7	6	ad4antr	⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝐺 ∈ UMGraph )
8		simpr	⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
9	8	anim1i	⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
10		3anass	⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
11	9 10	sylibr	⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
12	11	adantr	⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
13		simpr	⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
14	1 2	umgr3cyclex	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) )
15	7 12 13 14	syl3anc	⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) )
16	15	ex	⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) )
17	16	rexlimdvva	⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) )
18	17	ralimdva	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑣 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) ) )
19	3 18	mpd	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑣 ) )