Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (Revised by AV, 21-Oct-2020) (Proof shortened by AV, 7-Aug-2025)

	Ref	Expression
Hypotheses	usgrexmpl.v	|- V = ( 0 ... 4 )
	usgrexmpl.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
	usgrexmpl.g	|- G = <. V , E >.
Assertion	usgrexmpl	|- G e. USGraph

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	|- V = ( 0 ... 4 )
2		usgrexmpl.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
3		usgrexmpl.g	|- G = <. V , E >.
4	1 2	usgrexmplef	|- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }
5	3	eleq1i	|- ( G e. USGraph <-> <. V , E >. e. USGraph )
6	1	ovexi	|- V e. _V
7		s4cli	|- <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> e. Word _V
8	2 7	eqeltri	|- E e. Word _V
9		isusgrop	|- ( ( V e. _V /\ E e. Word _V ) -> ( <. V , E >. e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) )
10	6 8 9	mp2an	|- ( <. V , E >. e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
11	5 10	bitri	|- ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
12	4 11	mpbir	|- G e. USGraph