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

Metamath Proof Explorer

Theorem 1loopgruspgr

Description: A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop ). (Contributed by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v ⊢ φ → Vtx ⁡ G = V
1loopgruspgr.a ⊢ φ → A ∈ X
1loopgruspgr.n ⊢ φ → N ∈ V
1loopgruspgr.i ⊢ φ → iEdg ⁡ G = A N
Assertion 1loopgruspgr ⊢ φ → G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v ⊢ φ → Vtx ⁡ G = V
2 1loopgruspgr.a ⊢ φ → A ∈ X
3 1loopgruspgr.n ⊢ φ → N ∈ V
4 1loopgruspgr.i ⊢ φ → iEdg ⁡ G = A N
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 3 1 eleqtrrd ⊢ φ → N ∈ Vtx ⁡ G
7 dfsn2 ⊢ N = N N
8 7 a1i ⊢ φ → N = N N
9 8 opeq2d ⊢ φ → A N = A N N
10 9 sneqd ⊢ φ → A N = A N N
11 4 10 eqtrd ⊢ φ → iEdg ⁡ G = A N N
12 5 2 6 6 11 uspgr1e ⊢ φ → G ∈ USHGraph