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 GFriendGraphGConnGraph

Proof

Step Hyp Ref Expression
1 eqid VtxG=VtxG
2 1 2pthfrgr GFriendGraphkVtxGnVtxGkfpfkSPathsOnGnpf=2
3 spthonpthon fkSPathsOnGnpfkPathsOnGnp
4 3 adantr fkSPathsOnGnpf=2fkPathsOnGnp
5 4 2eximi fpfkSPathsOnGnpf=2fpfkPathsOnGnp
6 5 2ralimi kVtxGnVtxGkfpfkSPathsOnGnpf=2kVtxGnVtxGkfpfkPathsOnGnp
7 2 6 syl GFriendGraphkVtxGnVtxGkfpfkPathsOnGnp
8 1 isconngr1 GFriendGraphGConnGraphkVtxGnVtxGkfpfkPathsOnGnp
9 7 8 mpbird GFriendGraphGConnGraph