This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )