Metamath Proof Explorer

Theorem gropd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E ) has this property. (Contributed by AV, 11-Oct-2020)

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 )
Assertion gropd 
|- ( ph -> [. <. V , E >. / 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 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 )