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 ∈ V 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 fvexi ⊢ V ∈ V
4 hashgt12el2 ⊢ V ∈ V ∧ 1 < V ∧ a ∈ V → ∃ x ∈ V a ≠ x
5 3 4 mp3an1 ⊢ 1 < V ∧ a ∈ V → ∃ x ∈ V a ≠ 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 ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
12 6 9 10 11 syl3anc ⊢ x ∈ V ∧ a ≠ x ∧ a ∈ V ∧ G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
13 12 3exp1 ⊢ x ∈ V → a ≠ x → a ∈ V → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
14 13 rexlimiv ⊢ ∃ x ∈ V a ≠ x → a ∈ V → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
15 5 14 syl ⊢ 1 < V ∧ a ∈ V → a ∈ V → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
16 15 expcom ⊢ a ∈ V → 1 < V → a ∈ V → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
17 16 pm2.43a ⊢ a ∈ V → 1 < V → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
18 17 com13 ⊢ G ∈ FriendGraph → 1 < V → a ∈ V → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
19 18 imp ⊢ G ∈ FriendGraph ∧ 1 < V → a ∈ V → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
20 19 ralrimiv ⊢ G ∈ FriendGraph ∧ 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E