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 ∈ V b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ 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 ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
4 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
5 2 usgredgne ⊢ G ∈ USGraph ∧ b c ∈ E → b ≠ c
6 5 expcom ⊢ b c ∈ E → G ∈ USGraph → b ≠ c
7 6 3ad2ant2 ⊢ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → G ∈ USGraph → b ≠ c
8 4 7 syl5com ⊢ G ∈ FriendGraph → a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → b ≠ c
9 8 adantr ⊢ G ∈ FriendGraph ∧ 1 < V → a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → b ≠ c
10 9 ancrd ⊢ G ∈ FriendGraph ∧ 1 < V → a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
11 10 reximdv ⊢ G ∈ FriendGraph ∧ 1 < V → ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ c ∈ V b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
12 11 reximdv ⊢ G ∈ FriendGraph ∧ 1 < V → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
13 12 ralimdv ⊢ G ∈ FriendGraph ∧ 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
14 3 13 mpd ⊢ G ∈ FriendGraph ∧ 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E