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 ⊢ V = Vtx ⁡ G
isupgr.e ⊢ E = iEdg ⁡ G
Assertion upgrss ⊢ G ∈ UPGraph ∧ F ∈ dom ⁡ E → E ⁡ F ⊆ V

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ V = Vtx ⁡ G
2 isupgr.e ⊢ E = iEdg ⁡ G
3 ssrab2 ⊢ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ⊆ 𝒫 V ∖ ∅
4 difss ⊢ 𝒫 V ∖ ∅ ⊆ 𝒫 V
5 3 4 sstri ⊢ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ⊆ 𝒫 V
6 1 2 upgrf ⊢ G ∈ UPGraph → E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
7 6 ffvelrnda ⊢ G ∈ UPGraph ∧ F ∈ dom ⁡ E → E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
8 5 7 sseldi ⊢ G ∈ UPGraph ∧ F ∈ dom ⁡ E → E ⁡ F ∈ 𝒫 V
9 8 elpwid ⊢ G ∈ UPGraph ∧ F ∈ dom ⁡ E → E ⁡ F ⊆ V