Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v ⊢V=Vtx⁡G
2 3cyclfrgrrn1.e ⊢E=Edg⁡G
3 1 2 3cyclfrgrrn ⊢G∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
4 frgrusgr ⊢G∈FriendGraph→G∈USGraph
5 2 usgredgne ⊢G∈USGraph∧bc∈E→b≠c
6 5 expcom ⊢bc∈E→G∈USGraph→b≠c
7 6 3ad2ant2 ⊢ab∈E∧bc∈E∧ca∈E→G∈USGraph→b≠c
8 4 7 syl5com ⊢G∈FriendGraph→ab∈E∧bc∈E∧ca∈E→b≠c
9 8 adantr ⊢G∈FriendGraph∧1<V→ab∈E∧bc∈E∧ca∈E→b≠c
10 9 ancrd ⊢G∈FriendGraph∧1<V→ab∈E∧bc∈E∧ca∈E→b≠c∧ab∈E∧bc∈E∧ca∈E
11 10 reximdv ⊢G∈FriendGraph∧1<V→∃c∈Vab∈E∧bc∈E∧ca∈E→∃c∈Vb≠c∧ab∈E∧bc∈E∧ca∈E
12 11 reximdv ⊢G∈FriendGraph∧1<V→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E→∃b∈V∃c∈Vb≠c∧ab∈E∧bc∈E∧ca∈E
13 12 ralimdv ⊢G∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈E∧bc∈E∧ca∈E
14 3 13 mpd ⊢G∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈E∧bc∈E∧ca∈E