Metamath Proof Explorer


Theorem uhgrss

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 𝐸 ) → ( 𝐸𝐹 ) ⊆ 𝑉 )

Proof

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 𝐸 ) → ( 𝐸𝐹 ) ⊆ 𝑉 )