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	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ ConnGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	2pthfrgr	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑘 ( SPathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
3		spthonpthon	⊢ ( 𝑓 ( 𝑘 ( SPathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 → 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
4	3	adantr	⊢ ( ( 𝑓 ( 𝑘 ( SPathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
5	4	2eximi	⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑘 ( SPathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
6	5	2ralimi	⊢ ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑘 ( SPathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
7	2 6	syl	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
8	1	isconngr1	⊢ ( 𝐺 ∈ FriendGraph → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
9	7 8	mpbird	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ ConnGraph )