This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )