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

Metamath Proof Explorer

Theorem lppthon

Description: A loop (which is an edge at index J ) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021)

Ref Expression
Hypothesis lppthon.i 
|- I = ( iEdg ` G )
Assertion lppthon 
|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A ( PathsOn ` G ) A ) <" A A "> )

Proof

Step Hyp Ref Expression
1 lppthon.i 
 |-  I = ( iEdg ` G )
2 eqid 
 |-  <" A A "> = <" A A ">
3 eqid 
 |-  <" J "> = <" J ">
4 1 lpvtx 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) )
5 simpl3 
 |-  ( ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) /\ A = A ) -> ( I ` J ) = { A } )
6 eqid 
 |-  A = A
7 eqneqall 
 |-  ( A = A -> ( A =/= A -> { A , A } C_ ( I ` J ) ) )
8 6 7 ax-mp 
 |-  ( A =/= A -> { A , A } C_ ( I ` J ) )
9 8 adantl 
 |-  ( ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) /\ A =/= A ) -> { A , A } C_ ( I ` J ) )
10 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
11 2 3 4 4 5 9 10 1 1pthond 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A ( PathsOn ` G ) A ) <" A A "> )