Metamath Proof Explorer


Theorem grstructd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E ) has this property. (Contributed by AV, 12-Oct-2020) (Revised by AV, 9-Jun-2021)

Ref Expression
Hypotheses gropd.g
|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) )
gropd.v
|- ( ph -> V e. U )
gropd.e
|- ( ph -> E e. W )
grstructd.s
|- ( ph -> S e. X )
grstructd.f
|- ( ph -> Fun ( S \ { (/) } ) )
grstructd.d
|- ( ph -> 2 <_ ( # ` dom S ) )
grstructd.b
|- ( ph -> ( Base ` S ) = V )
grstructd.e
|- ( ph -> ( .ef ` S ) = E )
Assertion grstructd
|- ( ph -> [. S / g ]. ps )

Proof

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 )