Theorem grstructeld

Description: If any representation of a graph with vertices V and edges E is an element of an arbitrary class C , 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 ) is an element of this class C . (Contributed by AV, 12-Oct-2020) (Revised by AV, 9-Jun-2021)

	Ref	Expression
Hypotheses	gropeld.g	$$⊢\phi \to \forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to g\in C\right)$$
	gropeld.v	$$⊢\phi \to V\in U$$
	gropeld.e	$$⊢\phi \to E\in W$$
	grstructeld.s	$$⊢\phi \to S\in X$$
	grstructeld.f	$$⊢\phi \to \mathrm{Fun}\left(S\setminus \left\{\varnothing \right\}\right)$$
	grstructeld.d	$$⊢\phi \to 2\le \left|\mathrm{dom}S\right|$$
	grstructeld.b	$$⊢\phi \to {\mathrm{Base}}_S=V$$
	grstructeld.e	$$⊢\phi \to \mathrm{ef}\left(S\right)=E$$
Assertion	grstructeld	$$⊢\phi \to S\in C$$

Proof

Step	Hyp	Ref	Expression
1		gropeld.g	$$⊢\phi \to \forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to g\in C\right)$$
2		gropeld.v	$$⊢\phi \to V\in U$$
3		gropeld.e	$$⊢\phi \to E\in W$$
4		grstructeld.s	$$⊢\phi \to S\in X$$
5		grstructeld.f	$$⊢\phi \to \mathrm{Fun}\left(S\setminus \left\{\varnothing \right\}\right)$$
6		grstructeld.d	$$⊢\phi \to 2\le \left|\mathrm{dom}S\right|$$
7		grstructeld.b	$$⊢\phi \to {\mathrm{Base}}_S=V$$
8		grstructeld.e	$$⊢\phi \to \mathrm{ef}\left(S\right)=E$$
9	1 2 3 4 5 6 7 8	grstructd	$$⊢\phi \to \underset{\dot{}}{[}S/g\underset{\dot{}}{]}g\in C$$
10		sbcel1v	$$⊢\underset{\dot{}}{[}S/g\underset{\dot{}}{]}g\in C\leftrightarrow S\in C$$
11	9 10	sylib	$$⊢\phi \to S\in C$$