Theorem 0conngr

Description: A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

	Ref	Expression
Assertion	0conngr	$$⊢\varnothing \in \mathrm{ConnGraph}$$

Proof

Step	Hyp	Ref	Expression
1		ral0	$$⊢\forall k\in \varnothing \forall n\in \varnothing \exists f\exists pf\left(k\mathrm{PathsOn}\left(\varnothing \right)n\right)p$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		vtxval0	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$
4	3	eqcomi	$$⊢\varnothing =\mathrm{Vtx}\left(\varnothing \right)$$
5	4	isconngr	$$⊢\varnothing \in \mathrm{V}\to \left(\varnothing \in \mathrm{ConnGraph}\leftrightarrow \forall k\in \varnothing \forall n\in \varnothing \exists f\exists pf\left(k\mathrm{PathsOn}\left(\varnothing \right)n\right)p\right)$$
6	2 5	ax-mp	$$⊢\varnothing \in \mathrm{ConnGraph}\leftrightarrow \forall k\in \varnothing \forall n\in \varnothing \exists f\exists pf\left(k\mathrm{PathsOn}\left(\varnothing \right)n\right)p$$
7	1 6	mpbir	$$⊢\varnothing \in \mathrm{ConnGraph}$$