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

Metamath Proof Explorer

Theorem usgrausgri

Description: A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020)

Ref Expression
Hypothesis ausgr.1 
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
Assertion usgrausgri 
|- ( H e. USGraph -> ( Vtx ` H ) G ( Edg ` H ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 
 |-  G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2 usgredgss 
 |-  ( H e. USGraph -> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
3 fvex 
 |-  ( Vtx ` H ) e. _V
4 fvex 
 |-  ( Edg ` H ) e. _V
5 1 isausgr 
 |-  ( ( ( Vtx ` H ) e. _V /\ ( Edg ` H ) e. _V ) -> ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
6 3 4 5 mp2an 
 |-  ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
7 2 6 sylibr 
 |-  ( H e. USGraph -> ( Vtx ` H ) G ( Edg ` H ) )