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	|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> g e. C ) )
	gropeld.v	|- ( ph -> V e. U )
	gropeld.e	|- ( ph -> E e. W )
	grstructeld.s	|- ( ph -> S e. X )
	grstructeld.f	|- ( ph -> Fun ( S \ { (/) } ) )
	grstructeld.d	|- ( ph -> 2 <_ ( # ` dom S ) )
	grstructeld.b	|- ( ph -> ( Base ` S ) = V )
	grstructeld.e	|- ( ph -> ( .ef ` S ) = E )
Assertion	grstructeld	|- ( ph -> S e. C )

Proof

Step	Hyp	Ref	Expression
1		gropeld.g	|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> g e. C ) )
2		gropeld.v	|- ( ph -> V e. U )
3		gropeld.e	|- ( ph -> E e. W )
4		grstructeld.s	|- ( ph -> S e. X )
5		grstructeld.f	|- ( ph -> Fun ( S \ { (/) } ) )
6		grstructeld.d	|- ( ph -> 2 <_ ( # ` dom S ) )
7		grstructeld.b	|- ( ph -> ( Base ` S ) = V )
8		grstructeld.e	|- ( ph -> ( .ef ` S ) = E )
9	1 2 3 4 5 6 7 8	grstructd	|- ( ph -> [. S / g ]. g e. C )
10		sbcel1v	|- ( [. S / g ]. g e. C <-> S e. C )
11	9 10	sylib	|- ( ph -> S e. C )