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 
|- ( ph -> ( Vtx ` G ) = V )
1loopgruspgr.a 
|- ( ph -> A e. X )
1loopgruspgr.n 
|- ( ph -> N e. V )
1loopgruspgr.i 
|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
Assertion 1loopgruspgr 
|- ( ph -> G e. USPGraph )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v 
 |-  ( ph -> ( Vtx ` G ) = V )
2 1loopgruspgr.a 
 |-  ( ph -> A e. X )
3 1loopgruspgr.n 
 |-  ( ph -> N e. V )
4 1loopgruspgr.i 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 3 1 eleqtrrd 
 |-  ( ph -> N e. ( Vtx ` G ) )
7 dfsn2 
 |-  { N } = { N , N }
8 7 a1i 
 |-  ( ph -> { N } = { N , N } )
9 8 opeq2d 
 |-  ( ph -> <. A , { N } >. = <. A , { N , N } >. )
10 9 sneqd 
 |-  ( ph -> { <. A , { N } >. } = { <. A , { N , N } >. } )
11 4 10 eqtrd 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { N , N } >. } )
12 5 2 6 6 11 uspgr1e 
 |-  ( ph -> G e. USPGraph )