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 ⊢V=Vtx⁡G
Assertion 3cyclfrgr ⊢G∈FriendGraph∧1<V→∀v∈V∃f∃pfCycles⁡Gp∧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∈FriendGraph∧1<V→∀v∈V∃b∈V∃c∈Vvb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G
4 frgrusgr ⊢G∈FriendGraph→G∈USGraph
5 usgrumgr ⊢G∈USGraph→G∈UMGraph
6 4 5 syl ⊢G∈FriendGraph→G∈UMGraph
7 6 ad4antr ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V∧vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→G∈UMGraph
8 simpr ⊢G∈FriendGraph∧1<V∧v∈V→v∈V
9 8 anim1i ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V→v∈V∧b∈V∧c∈V
10 3anass ⊢v∈V∧b∈V∧c∈V↔v∈V∧b∈V∧c∈V
11 9 10 sylibr ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V→v∈V∧b∈V∧c∈V
12 11 adantr ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V∧vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→v∈V∧b∈V∧c∈V
13 simpr ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V∧vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G
14 1 2 umgr3cyclex ⊢G∈UMGraph∧v∈V∧b∈V∧c∈V∧vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v
15 7 12 13 14 syl3anc ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V∧vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v
16 15 ex ⊢G∈FriendGraph∧1<V∧v∈V∧b∈V∧c∈V→vb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v
17 16 rexlimdvva ⊢G∈FriendGraph∧1<V∧v∈V→∃b∈V∃c∈Vvb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v
18 17 ralimdva ⊢G∈FriendGraph∧1<V→∀v∈V∃b∈V∃c∈Vvb∈Edg⁡G∧bc∈Edg⁡G∧cv∈Edg⁡G→∀v∈V∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v
19 3 18 mpd ⊢G∈FriendGraph∧1<V→∀v∈V∃f∃pfCycles⁡Gp∧f=3∧p⁡0=v