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	ffvelcdmda	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
5	4	eldifad	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ 𝒫 𝑉 )
6	5	elpwid	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )