Metamath Proof Explorer

Theorem usgrexmpl1edg

Description: The edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } , { 0 , 3 } , { 3 , 4 } , { 3 , 5 } , { 4 , 5 } of the graph G = <. V , E >. . (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 usgrexmpl1edg 
|- ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )

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 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` <. V , E >. )
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 opiedgfv 
 |-  ( ( V e. _V /\ E e. Word _V ) -> ( iEdg ` <. V , E >. ) = E )
10 6 8 9 mp2an 
 |-  ( iEdg ` <. V , E >. ) = E
11 5 10 eqtri 
 |-  ( iEdg ` G ) = E
12 11 rneqi 
 |-  ran ( iEdg ` G ) = ran E
13 2 rneqi 
 |-  ran E = ran <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
14 prex 
 |-  { 0 , 1 } e. _V
15 id 
 |-  ( { 0 , 1 } e. _V -> { 0 , 1 } e. _V )
16 prex 
 |-  { 0 , 2 } e. _V
17 16 a1i 
 |-  ( { 0 , 1 } e. _V -> { 0 , 2 } e. _V )
18 prex 
 |-  { 1 , 2 } e. _V
19 18 a1i 
 |-  ( { 0 , 1 } e. _V -> { 1 , 2 } e. _V )
20 prex 
 |-  { 0 , 3 } e. _V
21 20 a1i 
 |-  ( { 0 , 1 } e. _V -> { 0 , 3 } e. _V )
22 prex 
 |-  { 3 , 4 } e. _V
23 22 a1i 
 |-  ( { 0 , 1 } e. _V -> { 3 , 4 } e. _V )
24 prex 
 |-  { 3 , 5 } e. _V
25 24 a1i 
 |-  ( { 0 , 1 } e. _V -> { 3 , 5 } e. _V )
26 prex 
 |-  { 4 , 5 } e. _V
27 26 a1i 
 |-  ( { 0 , 1 } e. _V -> { 4 , 5 } e. _V )
28 15 17 19 21 23 25 27 s7rn 
 |-  ( { 0 , 1 } e. _V -> ran <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } "> = ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 0 , 3 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
29 14 28 ax-mp 
 |-  ran <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } "> = ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 0 , 3 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
30 uncom 
 |-  ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 0 , 3 } } ) = ( { { 0 , 3 } } u. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } )
31 30 uneq1i 
 |-  ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 0 , 3 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) = ( ( { { 0 , 3 } } u. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
32 unass 
 |-  ( ( { { 0 , 3 } } u. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
33 31 32 eqtri 
 |-  ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 0 , 3 } } ) u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
34 13 29 33 3eqtri 
 |-  ran E = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
35 4 12 34 3eqtri 
 |-  ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )