Metamath Proof Explorer
Description: G is a simple graph of six vertices 0 , 1 , 2 , 3 , 4 , 5 , with
edges { 0 , 1 } , { 1 , 2 } , { 2 , 3 } , { 0 , 3 } , { 3 , 4 } ,
{ 4 , 5 } , { 0 , 5 } . (Contributed by AV, 3-Aug-2025)
|
|
Ref |
Expression |
|
Hypotheses |
usgrexmpl2.v |
|- V = ( 0 ... 5 ) |
|
|
usgrexmpl2.e |
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> |
|
|
usgrexmpl2.g |
|- G = <. V , E >. |
|
Assertion |
usgrexmpl2 |
|- G e. USGraph |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
usgrexmpl2.v |
|- V = ( 0 ... 5 ) |
| 2 |
|
usgrexmpl2.e |
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> |
| 3 |
|
usgrexmpl2.g |
|- G = <. V , E >. |
| 4 |
1 2
|
usgrexmpl2lem |
|- 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 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 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 |