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

Metamath Proof Explorer

Theorem lp1cycl

Description: A loop (which is an edge at index J ) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 lppthon.i 
 |-  I = ( iEdg ` G )
2 1 lppthon 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A ( PathsOn ` G ) A ) <" A A "> )
3 pthonispth 
 |-  ( <" J "> ( A ( PathsOn ` G ) A ) <" A A "> -> <" J "> ( Paths ` G ) <" A A "> )
4 2 3 syl 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( Paths ` G ) <" A A "> )
5 1 lpvtx 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) )
6 s2fv1 
 |-  ( A e. ( Vtx ` G ) -> ( <" A A "> ` 1 ) = A )
7 s1len 
 |-  ( # ` <" J "> ) = 1
8 7 fveq2i 
 |-  ( <" A A "> ` ( # ` <" J "> ) ) = ( <" A A "> ` 1 )
9 8 a1i 
 |-  ( A e. ( Vtx ` G ) -> ( <" A A "> ` ( # ` <" J "> ) ) = ( <" A A "> ` 1 ) )
10 s2fv0 
 |-  ( A e. ( Vtx ` G ) -> ( <" A A "> ` 0 ) = A )
11 6 9 10 3eqtr4rd 
 |-  ( A e. ( Vtx ` G ) -> ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) )
12 5 11 syl 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) )
13 iscycl 
 |-  ( <" J "> ( Cycles ` G ) <" A A "> <-> ( <" J "> ( Paths ` G ) <" A A "> /\ ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) ) )
14 4 12 13 sylanbrc 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( Cycles ` G ) <" A A "> )