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	$$⊢\phi \to \forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to \psi \right)$$
	gropd.v	$$⊢\phi \to V\in U$$
	gropd.e	$$⊢\phi \to E\in W$$
Assertion	gropd	$$⊢\phi \to \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi$$

Proof

Step	Hyp	Ref	Expression
1		gropd.g	$$⊢\phi \to \forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to \psi \right)$$
2		gropd.v	$$⊢\phi \to V\in U$$
3		gropd.e	$$⊢\phi \to E\in W$$
4		opex	$$⊢⟨V,E⟩\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to ⟨V,E⟩\in \mathrm{V}$$
6		opvtxfv	$$⊢\left(V\in U\wedge E\in W\right)\to \mathrm{Vtx}\left(⟨V,E⟩\right)=V$$
7		opiedgfv	$$⊢\left(V\in U\wedge E\in W\right)\to \mathrm{iEdg}\left(⟨V,E⟩\right)=E$$
8	6 7	jca	$$⊢\left(V\in U\wedge E\in W\right)\to \left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)$$
9	2 3 8	syl2anc	$$⊢\phi \to \left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}g⟨V,E⟩$$
11		nfv	$$⊢Ⅎg\left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)$$
12		nfsbc1v	$$⊢Ⅎg\underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi$$
13	11 12	nfim	$$⊢Ⅎg\left(\left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)\to \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi \right)$$
14		fveqeq2	$$⊢g=⟨V,E⟩\to \left(\mathrm{Vtx}\left(g\right)=V\leftrightarrow \mathrm{Vtx}\left(⟨V,E⟩\right)=V\right)$$
15		fveqeq2	$$⊢g=⟨V,E⟩\to \left(\mathrm{iEdg}\left(g\right)=E\leftrightarrow \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)$$
16	14 15	anbi12d	$$⊢g=⟨V,E⟩\to \left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\leftrightarrow \left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)\right)$$
17		sbceq1a	$$⊢g=⟨V,E⟩\to \left(\psi \leftrightarrow \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi \right)$$
18	16 17	imbi12d	$$⊢g=⟨V,E⟩\to \left(\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to \psi \right)\leftrightarrow \left(\left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)\to \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi \right)\right)$$
19	10 13 18	spcgf	$$⊢⟨V,E⟩\in \mathrm{V}\to \left(\forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to \psi \right)\to \left(\left(\mathrm{Vtx}\left(⟨V,E⟩\right)=V\wedge \mathrm{iEdg}\left(⟨V,E⟩\right)=E\right)\to \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi \right)\right)$$
20	5 1 9 19	syl3c	$$⊢\phi \to \underset{\dot{}}{[}⟨V,E⟩/g\underset{\dot{}}{]}\psi$$