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