Metamath Proof Explorer

Theorem uhgrn0

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

Ref Expression
Hypothesis uhgrfun.e ⊢ E = iEdg ⁡ G
Assertion uhgrn0 ⊢ G ∈ UHGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≠ ∅

Proof

Step Hyp Ref Expression
1 uhgrfun.e ⊢ E = iEdg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 1 uhgrf ⊢ G ∈ UHGraph → E : dom ⁡ E ⟶ 𝒫 Vtx ⁡ G ∖ ∅
4 fndm ⊢ E Fn A → dom ⁡ E = A
5 4 feq2d ⊢ E Fn A → E : dom ⁡ E ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ↔ E : A ⟶ 𝒫 Vtx ⁡ G ∖ ∅
6 3 5 syl5ibcom ⊢ G ∈ UHGraph → E Fn A → E : A ⟶ 𝒫 Vtx ⁡ G ∖ ∅
7 6 imp ⊢ G ∈ UHGraph ∧ E Fn A → E : A ⟶ 𝒫 Vtx ⁡ G ∖ ∅
8 7 ffvelcdmda ⊢ G ∈ UHGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ 𝒫 Vtx ⁡ G ∖ ∅
9 8 3impa ⊢ G ∈ UHGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ 𝒫 Vtx ⁡ G ∖ ∅
10 eldifsni ⊢ E ⁡ F ∈ 𝒫 Vtx ⁡ G ∖ ∅ → E ⁡ F ≠ ∅
11 9 10 syl ⊢ G ∈ UHGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≠ ∅