Theorem 1pthon2ve

Description: For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021) (Proof shortened by AV, 15-Feb-2021)

	Ref	Expression
Hypotheses	1pthon2v.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	1pthon2v.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	1pthon2ve	$$⊢\left(G\in \mathrm{UHGraph}\wedge \left(A\in V\wedge B\in V\right)\wedge \left\{A,B\right\}\in E\right)\to \exists f\exists pf\left(A\mathrm{PathsOn}\left(G\right)B\right)p$$

Proof

Step	Hyp	Ref	Expression
1		1pthon2v.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		1pthon2v.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		id	$$⊢\left\{A,B\right\}\in E\to \left\{A,B\right\}\in E$$
4		sseq2	$$⊢e=\left\{A,B\right\}\to \left(\left\{A,B\right\}\subseteq e\leftrightarrow \left\{A,B\right\}\subseteq \left\{A,B\right\}\right)$$
5	4	adantl	$$⊢\left(\left\{A,B\right\}\in E\wedge e=\left\{A,B\right\}\right)\to \left(\left\{A,B\right\}\subseteq e\leftrightarrow \left\{A,B\right\}\subseteq \left\{A,B\right\}\right)$$
6		ssidd	$$⊢\left\{A,B\right\}\in E\to \left\{A,B\right\}\subseteq \left\{A,B\right\}$$
7	3 5 6	rspcedvd	$$⊢\left\{A,B\right\}\in E\to \exists e\in E\left\{A,B\right\}\subseteq e$$
8	1 2	1pthon2v	$$⊢\left(G\in \mathrm{UHGraph}\wedge \left(A\in V\wedge B\in V\right)\wedge \exists e\in E\left\{A,B\right\}\subseteq e\right)\to \exists f\exists pf\left(A\mathrm{PathsOn}\left(G\right)B\right)p$$
9	7 8	syl3an3	$$⊢\left(G\in \mathrm{UHGraph}\wedge \left(A\in V\wedge B\in V\right)\wedge \left\{A,B\right\}\in E\right)\to \exists f\exists pf\left(A\mathrm{PathsOn}\left(G\right)B\right)p$$