Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 18-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uhgrf.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
uhgrf.e | ⊢ 𝐸 = ( iEdg ‘ 𝐺 ) | ||
Assertion | uhgrss | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uhgrf.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | uhgrf.e | ⊢ 𝐸 = ( iEdg ‘ 𝐺 ) | |
3 | 1 2 | uhgrf | ⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) |
4 | 3 | ffvelrnda | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ) |
5 | 4 | eldifad | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ 𝒫 𝑉 ) |
6 | 5 | elpwid | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 ) |