Metamath Proof Explorer


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 ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝑔𝐶 ) )
gropeld.v ( 𝜑𝑉𝑈 )
gropeld.e ( 𝜑𝐸𝑊 )
grstructeld.s ( 𝜑𝑆𝑋 )
grstructeld.f ( 𝜑 → Fun ( 𝑆 ∖ { ∅ } ) )
grstructeld.d ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝑆 ) )
grstructeld.b ( 𝜑 → ( Base ‘ 𝑆 ) = 𝑉 )
grstructeld.e ( 𝜑 → ( .ef ‘ 𝑆 ) = 𝐸 )
Assertion grstructeld ( 𝜑𝑆𝐶 )

Proof

Step Hyp Ref Expression
1 gropeld.g ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝑔𝐶 ) )
2 gropeld.v ( 𝜑𝑉𝑈 )
3 gropeld.e ( 𝜑𝐸𝑊 )
4 grstructeld.s ( 𝜑𝑆𝑋 )
5 grstructeld.f ( 𝜑 → Fun ( 𝑆 ∖ { ∅ } ) )
6 grstructeld.d ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝑆 ) )
7 grstructeld.b ( 𝜑 → ( Base ‘ 𝑆 ) = 𝑉 )
8 grstructeld.e ( 𝜑 → ( .ef ‘ 𝑆 ) = 𝐸 )
9 1 2 3 4 5 6 7 8 grstructd ( 𝜑[ 𝑆 / 𝑔 ] 𝑔𝐶 )
10 sbcel1v ( [ 𝑆 / 𝑔 ] 𝑔𝐶𝑆𝐶 )
11 9 10 sylib ( 𝜑𝑆𝐶 )