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 |
1 2
|
usgrexmplef |
|- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } |
5 |
|
opex |
|- <. V , E >. e. _V |
6 |
3 5
|
eqeltri |
|- G e. _V |
7 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
8 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
9 |
7 8
|
isusgrs |
|- ( G e. _V -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) ) |
10 |
1 2 3
|
usgrexmpllem |
|- ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) |
11 |
|
simpr |
|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( iEdg ` G ) = E ) |
12 |
11
|
dmeqd |
|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> dom ( iEdg ` G ) = dom E ) |
13 |
|
pweq |
|- ( ( Vtx ` G ) = V -> ~P ( Vtx ` G ) = ~P V ) |
14 |
13
|
adantr |
|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ~P ( Vtx ` G ) = ~P V ) |
15 |
14
|
rabeqdv |
|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } = { e e. ~P V | ( # ` e ) = 2 } ) |
16 |
11 12 15
|
f1eq123d |
|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) ) |
17 |
10 16
|
ax-mp |
|- ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) |
18 |
9 17
|
syl6bb |
|- ( G e. _V -> ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) ) |
19 |
6 18
|
ax-mp |
|- ( G e. USGraph <-> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } ) |
20 |
4 19
|
mpbir |
|- G e. USGraph |