Metamath Proof Explorer

Theorem frgrconngr

Description: A friendship graph is connected, see remark 1 in MertziosUnger p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 1-Apr-2021)

Ref Expression
Assertion frgrconngr ⊢ G ∈ FriendGraph → G ∈ ConnGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 2pthfrgr ⊢ G ∈ FriendGraph → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ k ∃ f ∃ p f k SPathsOn ⁡ G n p ∧ f = 2
3 spthonpthon ⊢ f k SPathsOn ⁡ G n p → f k PathsOn ⁡ G n p
4 3 adantr ⊢ f k SPathsOn ⁡ G n p ∧ f = 2 → f k PathsOn ⁡ G n p
5 4 2eximi ⊢ ∃ f ∃ p f k SPathsOn ⁡ G n p ∧ f = 2 → ∃ f ∃ p f k PathsOn ⁡ G n p
6 5 2ralimi ⊢ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ k ∃ f ∃ p f k SPathsOn ⁡ G n p ∧ f = 2 → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
7 2 6 syl ⊢ G ∈ FriendGraph → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
8 1 isconngr1 ⊢ G ∈ FriendGraph → G ∈ ConnGraph ↔ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
9 7 8 mpbird ⊢ G ∈ FriendGraph → G ∈ ConnGraph