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)

	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		opex	|- <. V , E >. e. _V
6	3 5	eqeltri	|- G e. _V
7		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
8		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
9	7 8	isusgrs	|- ( G e. _V -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) )
10	1 2 3	usgrexmpllem	|- ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )
11		simpr	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( iEdg ` G ) = E )
12	11	dmeqd	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> dom ( iEdg ` G ) = dom E )
13		pweq	|- ( ( Vtx ` G ) = V -> ~P ( Vtx ` G ) = ~P V )
14	13	adantr	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ~P ( Vtx ` G ) = ~P V )
15	14	rabeqdv	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } = { e e. ~P V | ( # ` e ) = 2 } )
16	11 12 15	f1eq123d	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) )
17	10 16	ax-mp	|- ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
18	9 17	syl6bb	|- ( G e. _V -> ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) )
19	6 18	ax-mp	|- ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
20	4 19	mpbir	|- G e. USGraph