Metamath Proof Explorer

Theorem usgrexmpl2edg

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

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 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` <. V , E >. )
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 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 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
14 prex 
 |-  { 0 , 1 } e. _V
15 id 
 |-  ( { 0 , 1 } e. _V -> { 0 , 1 } e. _V )
16 prex 
 |-  { 1 , 2 } e. _V
17 16 a1i 
 |-  ( { 0 , 1 } e. _V -> { 1 , 2 } e. _V )
18 prex 
 |-  { 2 , 3 } e. _V
19 18 a1i 
 |-  ( { 0 , 1 } e. _V -> { 2 , 3 } e. _V )
20 prex 
 |-  { 3 , 4 } e. _V
21 20 a1i 
 |-  ( { 0 , 1 } e. _V -> { 3 , 4 } e. _V )
22 prex 
 |-  { 4 , 5 } e. _V
23 22 a1i 
 |-  ( { 0 , 1 } e. _V -> { 4 , 5 } e. _V )
24 prex 
 |-  { 0 , 3 } e. _V
25 24 a1i 
 |-  ( { 0 , 1 } e. _V -> { 0 , 3 } e. _V )
26 prex 
 |-  { 0 , 5 } e. _V
27 26 a1i 
 |-  ( { 0 , 1 } e. _V -> { 0 , 5 } e. _V )
28 15 17 19 21 23 25 27 s7rn 
 |-  ( { 0 , 1 } e. _V -> ran <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> = ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
29 14 28 ax-mp 
 |-  ran <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> = ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } )
30 unass 
 |-  ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) = ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. ( { { 3 , 4 } } u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
31 df-tp 
 |-  { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } = ( { { 4 , 5 } , { 0 , 3 } } u. { { 0 , 5 } } )
32 df-pr 
 |-  { { 4 , 5 } , { 0 , 3 } } = ( { { 4 , 5 } } u. { { 0 , 3 } } )
33 32 uneq1i 
 |-  ( { { 4 , 5 } , { 0 , 3 } } u. { { 0 , 5 } } ) = ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } )
34 31 33 eqtri 
 |-  { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } = ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } )
35 34 uneq2i 
 |-  ( { { 3 , 4 } } u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) = ( { { 3 , 4 } } u. ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } ) )
36 unass 
 |-  ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } ) = ( { { 4 , 5 } } u. ( { { 0 , 3 } } u. { { 0 , 5 } } ) )
37 uncom 
 |-  ( { { 4 , 5 } } u. ( { { 0 , 3 } } u. { { 0 , 5 } } ) ) = ( ( { { 0 , 3 } } u. { { 0 , 5 } } ) u. { { 4 , 5 } } )
38 unass 
 |-  ( ( { { 0 , 3 } } u. { { 0 , 5 } } ) u. { { 4 , 5 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) )
39 36 37 38 3eqtri 
 |-  ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) )
40 39 uneq2i 
 |-  ( { { 3 , 4 } } u. ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } ) ) = ( { { 3 , 4 } } u. ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) ) )
41 uncom 
 |-  ( { { 3 , 4 } } u. ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) ) ) = ( ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) ) u. { { 3 , 4 } } )
42 unass 
 |-  ( ( { { 0 , 3 } } u. ( { { 0 , 5 } } u. { { 4 , 5 } } ) ) u. { { 3 , 4 } } ) = ( { { 0 , 3 } } u. ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } ) )
43 40 41 42 3eqtri 
 |-  ( { { 3 , 4 } } u. ( ( { { 4 , 5 } } u. { { 0 , 3 } } ) u. { { 0 , 5 } } ) ) = ( { { 0 , 3 } } u. ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } ) )
44 df-tp 
 |-  { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } = ( { { 3 , 4 } , { 4 , 5 } } u. { { 0 , 5 } } )
45 uncom 
 |-  ( { { 3 , 4 } , { 4 , 5 } } u. { { 0 , 5 } } ) = ( { { 0 , 5 } } u. { { 3 , 4 } , { 4 , 5 } } )
46 df-pr 
 |-  { { 3 , 4 } , { 4 , 5 } } = ( { { 3 , 4 } } u. { { 4 , 5 } } )
47 46 equncomi 
 |-  { { 3 , 4 } , { 4 , 5 } } = ( { { 4 , 5 } } u. { { 3 , 4 } } )
48 47 uneq2i 
 |-  ( { { 0 , 5 } } u. { { 3 , 4 } , { 4 , 5 } } ) = ( { { 0 , 5 } } u. ( { { 4 , 5 } } u. { { 3 , 4 } } ) )
49 unass 
 |-  ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } ) = ( { { 0 , 5 } } u. ( { { 4 , 5 } } u. { { 3 , 4 } } ) )
50 48 49 eqtr4i 
 |-  ( { { 0 , 5 } } u. { { 3 , 4 } , { 4 , 5 } } ) = ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } )
51 44 45 50 3eqtrri 
 |-  ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } ) = { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } }
52 51 uneq2i 
 |-  ( { { 0 , 3 } } u. ( ( { { 0 , 5 } } u. { { 4 , 5 } } ) u. { { 3 , 4 } } ) ) = ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } )
53 35 43 52 3eqtri 
 |-  ( { { 3 , 4 } } u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) = ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } )
54 53 uneq2i 
 |-  ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. ( { { 3 , 4 } } u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ) = ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
55 54 equncomi 
 |-  ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. ( { { 3 , 4 } } u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ) = ( ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } )
56 unass 
 |-  ( ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ) = ( { { 0 , 3 } } u. ( { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ) )
57 uncom 
 |-  ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) = ( { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } )
58 57 uneq2i 
 |-  ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) = ( { { 0 , 3 } } u. ( { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ) )
59 56 58 eqtr4i 
 |-  ( ( { { 0 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) u. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
60 30 55 59 3eqtri 
 |-  ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
61 13 29 60 3eqtri 
 |-  ran E = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
62 4 12 61 3eqtri 
 |-  ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )