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

Metamath Proof Explorer

Theorem usgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypotheses usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
usgrss.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion usgrss ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 )

Proof

Step Hyp Ref Expression
1 usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 usgrss.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ 𝒫 𝑉
4 2 1 usgrfs ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 f1f ⊢ ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 4 5 syl ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 6 ffvelcdmda ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
8 3 7 sselid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ 𝒫 𝑉 )
9 8 elpwid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 )