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 |
|
grstructd.s |
|- ( ph -> S e. X ) |
5 |
|
grstructd.f |
|- ( ph -> Fun ( S \ { (/) } ) ) |
6 |
|
grstructd.d |
|- ( ph -> 2 <_ ( # ` dom S ) ) |
7 |
|
grstructd.b |
|- ( ph -> ( Base ` S ) = V ) |
8 |
|
grstructd.e |
|- ( ph -> ( .ef ` S ) = E ) |
9 |
|
funvtxdmge2val |
|- ( ( Fun ( S \ { (/) } ) /\ 2 <_ ( # ` dom S ) ) -> ( Vtx ` S ) = ( Base ` S ) ) |
10 |
5 6 9
|
syl2anc |
|- ( ph -> ( Vtx ` S ) = ( Base ` S ) ) |
11 |
10 7
|
eqtrd |
|- ( ph -> ( Vtx ` S ) = V ) |
12 |
|
funiedgdmge2val |
|- ( ( Fun ( S \ { (/) } ) /\ 2 <_ ( # ` dom S ) ) -> ( iEdg ` S ) = ( .ef ` S ) ) |
13 |
5 6 12
|
syl2anc |
|- ( ph -> ( iEdg ` S ) = ( .ef ` S ) ) |
14 |
13 8
|
eqtrd |
|- ( ph -> ( iEdg ` S ) = E ) |
15 |
11 14
|
jca |
|- ( ph -> ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) ) |
16 |
|
nfcv |
|- F/_ g S |
17 |
|
nfv |
|- F/ g ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) |
18 |
|
nfsbc1v |
|- F/ g [. S / g ]. ps |
19 |
17 18
|
nfim |
|- F/ g ( ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) -> [. S / g ]. ps ) |
20 |
|
fveqeq2 |
|- ( g = S -> ( ( Vtx ` g ) = V <-> ( Vtx ` S ) = V ) ) |
21 |
|
fveqeq2 |
|- ( g = S -> ( ( iEdg ` g ) = E <-> ( iEdg ` S ) = E ) ) |
22 |
20 21
|
anbi12d |
|- ( g = S -> ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) <-> ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) ) ) |
23 |
|
sbceq1a |
|- ( g = S -> ( ps <-> [. S / g ]. ps ) ) |
24 |
22 23
|
imbi12d |
|- ( g = S -> ( ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) <-> ( ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) -> [. S / g ]. ps ) ) ) |
25 |
16 19 24
|
spcgf |
|- ( S e. X -> ( A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) -> ( ( ( Vtx ` S ) = V /\ ( iEdg ` S ) = E ) -> [. S / g ]. ps ) ) ) |
26 |
4 1 15 25
|
syl3c |
|- ( ph -> [. S / g ]. ps ) |