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 \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ 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 \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to A \in Vtx (G)$
5		simpl3	$⊢ ((G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \land A = A) \to I (J) = \{A\}$
6		eqid	$⊢ A = A$
7		eqneqall	$⊢ A = A \to (A \neq A \to \{A, A\} \subseteq I (J))$
8	6 7	ax-mp	$⊢ A \neq A \to \{A, A\} \subseteq I (J)$
9	8	adantl	$⊢ ((G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \land A \neq A) \to \{A, A\} \subseteq I (J)$
10		eqid	$⊢ Vtx (G) = Vtx (G)$
11	2 3 4 4 5 9 10 1	1pthond	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ J ”⟩ (A PathsOn (G) A) ⟨“ A A ”⟩$