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 = ( Vtx ` G )
	1pthon2v.e	|- E = ( Edg ` G )
Assertion	1pthon2ve	|- ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ { A , B } e. E ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )

Proof

Step	Hyp	Ref	Expression
1		1pthon2v.v	|- V = ( Vtx ` G )
2		1pthon2v.e	|- E = ( Edg ` G )
3		id	|- ( { A , B } e. E -> { A , B } e. E )
4		sseq2	|- ( e = { A , B } -> ( { A , B } C_ e <-> { A , B } C_ { A , B } ) )
5	4	adantl	|- ( ( { A , B } e. E /\ e = { A , B } ) -> ( { A , B } C_ e <-> { A , B } C_ { A , B } ) )
6		ssidd	|- ( { A , B } e. E -> { A , B } C_ { A , B } )
7	3 5 6	rspcedvd	|- ( { A , B } e. E -> E. e e. E { A , B } C_ e )
8	1 2	1pthon2v	|- ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )
9	7 8	syl3an3	|- ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ { A , B } e. E ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )