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 UHGraph J dom I I J = A ⟨“ J ”⟩ A PathsOn G A ⟨“ AA ”⟩

Proof

Step Hyp Ref Expression
1 lppthon.i I = iEdg G
2 eqid ⟨“ AA ”⟩ = ⟨“ AA ”⟩
3 eqid ⟨“ J ”⟩ = ⟨“ J ”⟩
4 1 lpvtx G UHGraph J dom I I J = A A Vtx G
5 simpl3 G UHGraph J dom I I J = A A = A I J = A
6 eqid A = A
7 eqneqall A = A A A A A I J
8 6 7 ax-mp A A A A I J
9 8 adantl G UHGraph J dom I I J = A A A A A I J
10 eqid Vtx G = Vtx G
11 2 3 4 4 5 9 10 1 1pthond G UHGraph J dom I I J = A ⟨“ J ”⟩ A PathsOn G A ⟨“ AA ”⟩