Metamath Proof Explorer

Theorem upgrn0

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

Ref Expression
Hypotheses isupgr.v ⊢ V = Vtx ⁡ G
isupgr.e ⊢ E = iEdg ⁡ G
Assertion upgrn0 ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≠ ∅

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 1 2 upgrfn ⊢ G ∈ UPGraph ∧ E Fn A → E : A ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
5 4 ffvelrnda ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
6 5 3impa ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
7 3 6 sselid ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ 𝒫 V ∖ ∅
8 eldifsni ⊢ E ⁡ F ∈ 𝒫 V ∖ ∅ → E ⁡ F ≠ ∅
9 7 8 syl ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≠ ∅