Metamath Proof Explorer

Theorem usgrexmpledg

Description: The edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (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 usgrexmpledg 
|- ( Edg ` G ) = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )

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 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 1 2 3 usgrexmpllem 
 |-  ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )
6 5 simpri 
 |-  ( iEdg ` G ) = E
7 6 rneqi 
 |-  ran ( iEdg ` G ) = ran E
8 prex 
 |-  { 0 , 1 } e. _V
9 prex 
 |-  { 1 , 2 } e. _V
10 8 9 pm3.2i 
 |-  ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V )
11 prex 
 |-  { 2 , 0 } e. _V
12 prex 
 |-  { 0 , 3 } e. _V
13 11 12 pm3.2i 
 |-  ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V )
14 10 13 pm3.2i 
 |-  ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) )
15 usgrexmpldifpr 
 |-  ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) )
16 14 15 pm3.2i 
 |-  ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) /\ ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) )
17 16 2 pm3.2i 
 |-  ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) /\ ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> )
18 s4f1o 
 |-  ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) -> ( ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) ) )
19 18 imp31 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) /\ ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> ) -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
20 dff1o5 
 |-  ( E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) /\ ran E = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) )
21 20 simprbi 
 |-  ( E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> ran E = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
22 17 19 21 mp2b 
 |-  ran E = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )
23 4 7 22 3eqtri 
 |-  ( Edg ` G ) = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )