Step |
Hyp |
Ref |
Expression |
1 |
|
gropd.g |
|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) ) |
2 |
|
gropd.v |
|- ( ph -> V e. U ) |
3 |
|
gropd.e |
|- ( ph -> E e. W ) |
4 |
|
opex |
|- <. V , E >. e. _V |
5 |
4
|
a1i |
|- ( ph -> <. V , E >. e. _V ) |
6 |
|
opvtxfv |
|- ( ( V e. U /\ E e. W ) -> ( Vtx ` <. V , E >. ) = V ) |
7 |
|
opiedgfv |
|- ( ( V e. U /\ E e. W ) -> ( iEdg ` <. V , E >. ) = E ) |
8 |
6 7
|
jca |
|- ( ( V e. U /\ E e. W ) -> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) ) |
9 |
2 3 8
|
syl2anc |
|- ( ph -> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) ) |
10 |
|
nfcv |
|- F/_ g <. V , E >. |
11 |
|
nfv |
|- F/ g ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) |
12 |
|
nfsbc1v |
|- F/ g [. <. V , E >. / g ]. ps |
13 |
11 12
|
nfim |
|- F/ g ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps ) |
14 |
|
fveqeq2 |
|- ( g = <. V , E >. -> ( ( Vtx ` g ) = V <-> ( Vtx ` <. V , E >. ) = V ) ) |
15 |
|
fveqeq2 |
|- ( g = <. V , E >. -> ( ( iEdg ` g ) = E <-> ( iEdg ` <. V , E >. ) = E ) ) |
16 |
14 15
|
anbi12d |
|- ( g = <. V , E >. -> ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) <-> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) ) ) |
17 |
|
sbceq1a |
|- ( g = <. V , E >. -> ( ps <-> [. <. V , E >. / g ]. ps ) ) |
18 |
16 17
|
imbi12d |
|- ( g = <. V , E >. -> ( ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) <-> ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps ) ) ) |
19 |
10 13 18
|
spcgf |
|- ( <. V , E >. e. _V -> ( A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) -> ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps ) ) ) |
20 |
5 1 9 19
|
syl3c |
|- ( ph -> [. <. V , E >. / g ]. ps ) |