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 | ⊢ ( 𝜑 → 𝑆 ∈ 𝐶 ) |
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 | ⊢ ( 𝜑 → 𝑆 ∈ 𝐶 ) |