Metamath Proof Explorer

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∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v ⊢V=Vtx⁡G
2 3cyclfrgrrn1.e ⊢E=Edg⁡G
3 1 fvexi ⊢V∈V
4 hashgt12el2 ⊢V∈V∧1<V∧a∈V→∃x∈Va≠x
5 3 4 mp3an1 ⊢1<V∧a∈V→∃x∈Va≠x
6 simpr ⊢x∈V∧a≠x∧a∈V∧G∈FriendGraph→G∈FriendGraph
7 pm3.22 ⊢x∈V∧a∈V→a∈V∧x∈V
8 7 3adant2 ⊢x∈V∧a≠x∧a∈V→a∈V∧x∈V
9 8 adantr ⊢x∈V∧a≠x∧a∈V∧G∈FriendGraph→a∈V∧x∈V
10 simpl2 ⊢x∈V∧a≠x∧a∈V∧G∈FriendGraph→a≠x
11 1 2 3cyclfrgrrn1 ⊢G∈FriendGraph∧a∈V∧x∈V∧a≠x→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
12 6 9 10 11 syl3anc ⊢x∈V∧a≠x∧a∈V∧G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
13 12 3exp1 ⊢x∈V→a≠x→a∈V→G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
14 13 rexlimiv ⊢∃x∈Va≠x→a∈V→G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
15 5 14 syl ⊢1<V∧a∈V→a∈V→G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
16 15 expcom ⊢a∈V→1<V→a∈V→G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
17 16 pm2.43a ⊢a∈V→1<V→G∈FriendGraph→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
18 17 com13 ⊢G∈FriendGraph→1<V→a∈V→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
19 18 imp ⊢G∈FriendGraph∧1<V→a∈V→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
20 19 ralrimiv ⊢G∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E