Metamath Proof Explorer


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 ) = 𝑣 ) )