This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
8 5 7 sselid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ∈ 𝒫 𝑉 )
9 8 elpwid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )