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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	lppthon	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) ⟨“ 𝐴 𝐴 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		lppthon.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		eqid	⊢ ⟨“ 𝐴 𝐴 ”⟩ = ⟨“ 𝐴 𝐴 ”⟩
3		eqid	⊢ ⟨“ 𝐽 ”⟩ = ⟨“ 𝐽 ”⟩
4	1	lpvtx	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
5		simpl3	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) ∧ 𝐴 = 𝐴 ) → ( 𝐼 ‘ 𝐽 ) = { 𝐴 } )
6		eqid	⊢ 𝐴 = 𝐴
7		eqneqall	⊢ ( 𝐴 = 𝐴 → ( 𝐴 ≠ 𝐴 → { 𝐴 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
8	6 7	ax-mp	⊢ ( 𝐴 ≠ 𝐴 → { 𝐴 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
9	8	adantl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) ∧ 𝐴 ≠ 𝐴 ) → { 𝐴 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
10		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11	2 3 4 4 5 9 10 1	1pthond	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) ⟨“ 𝐴 𝐴 ”⟩ )