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 "> )