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

Metamath Proof Explorer

Theorem usgrexmpl1

Description: G is a simple graph of six vertices 0 , 1 , 2 , 3 , 4 , 5 , with edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } , { 0 , 3 } , { 3 , 4 } , { 3 , 5 } , { 4 , 5 } . (Contributed by AV, 3-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl1.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
3 usgrexmpl1.g 
 |-  G = <. V , E >.
4 1 2 usgrexmpl1lem 
 |-  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 s7cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } "> 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