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