Theorem upgrss

Description: An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 29-Nov-2020)

	Ref	Expression
Hypotheses	isupgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isupgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	upgrss	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isupgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		ssrab2	⊢ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ⊆ ( 𝒫 𝑉 ∖ { ∅ } )
4		difss	⊢ ( 𝒫 𝑉 ∖ { ∅ } ) ⊆ 𝒫 𝑉
5	3 4	sstri	⊢ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ⊆ 𝒫 𝑉
6	1 2	upgrf	⊢ ( 𝐺 ∈ UPGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
7	6	ffvelrnda	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
8	5 7	sselid	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ 𝒫 𝑉 )
9	8	elpwid	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )