Step |
Hyp |
Ref |
Expression |
1 |
|
isuhgr.v |
|- V = ( Vtx ` G ) |
2 |
|
isuhgr.e |
|- E = ( iEdg ` G ) |
3 |
|
df-ushgr |
|- USHGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) } |
4 |
3
|
eleq2i |
|- ( G e. USHGraph <-> G e. { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) } ) |
5 |
|
fveq2 |
|- ( h = G -> ( iEdg ` h ) = ( iEdg ` G ) ) |
6 |
5 2
|
eqtr4di |
|- ( h = G -> ( iEdg ` h ) = E ) |
7 |
5
|
dmeqd |
|- ( h = G -> dom ( iEdg ` h ) = dom ( iEdg ` G ) ) |
8 |
2
|
eqcomi |
|- ( iEdg ` G ) = E |
9 |
8
|
dmeqi |
|- dom ( iEdg ` G ) = dom E |
10 |
7 9
|
eqtrdi |
|- ( h = G -> dom ( iEdg ` h ) = dom E ) |
11 |
|
fveq2 |
|- ( h = G -> ( Vtx ` h ) = ( Vtx ` G ) ) |
12 |
11 1
|
eqtr4di |
|- ( h = G -> ( Vtx ` h ) = V ) |
13 |
12
|
pweqd |
|- ( h = G -> ~P ( Vtx ` h ) = ~P V ) |
14 |
13
|
difeq1d |
|- ( h = G -> ( ~P ( Vtx ` h ) \ { (/) } ) = ( ~P V \ { (/) } ) ) |
15 |
6 10 14
|
f1eq123d |
|- ( h = G -> ( ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) ) |
16 |
|
fvexd |
|- ( g = h -> ( Vtx ` g ) e. _V ) |
17 |
|
fveq2 |
|- ( g = h -> ( Vtx ` g ) = ( Vtx ` h ) ) |
18 |
|
fvexd |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) e. _V ) |
19 |
|
fveq2 |
|- ( g = h -> ( iEdg ` g ) = ( iEdg ` h ) ) |
20 |
19
|
adantr |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) = ( iEdg ` h ) ) |
21 |
|
simpr |
|- ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> e = ( iEdg ` h ) ) |
22 |
21
|
dmeqd |
|- ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> dom e = dom ( iEdg ` h ) ) |
23 |
|
simpr |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> v = ( Vtx ` h ) ) |
24 |
23
|
pweqd |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> ~P v = ~P ( Vtx ` h ) ) |
25 |
24
|
difeq1d |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> ( ~P v \ { (/) } ) = ( ~P ( Vtx ` h ) \ { (/) } ) ) |
26 |
25
|
adantr |
|- ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ( ~P v \ { (/) } ) = ( ~P ( Vtx ` h ) \ { (/) } ) ) |
27 |
21 22 26
|
f1eq123d |
|- ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ( e : dom e -1-1-> ( ~P v \ { (/) } ) <-> ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) ) ) |
28 |
18 20 27
|
sbcied2 |
|- ( ( g = h /\ v = ( Vtx ` h ) ) -> ( [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) <-> ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) ) ) |
29 |
16 17 28
|
sbcied2 |
|- ( g = h -> ( [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) <-> ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) ) ) |
30 |
29
|
cbvabv |
|- { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) } = { h | ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) } |
31 |
15 30
|
elab2g |
|- ( G e. U -> ( G e. { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) } <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) ) |
32 |
4 31
|
syl5bb |
|- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) ) |