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 \in UHGraph \land E Fn A \land F \in A) \to E (F) \neq \emptyset$

Step	Hyp	Ref	Expression
1		uhgrfun.e	$⊢ E = iEdg (G)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2 1	uhgrf	$⊢ G \in UHGraph \to E : dom E ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\}$
4		fndm	$⊢ E Fn A \to dom E = A$
5	4	feq2d	$⊢ E Fn A \to (E : dom E ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\} \leftrightarrow E : A ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\})$
6	3 5	syl5ibcom	$⊢ G \in UHGraph \to (E Fn A \to E : A ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\})$
7	6	imp	$⊢ (G \in UHGraph \land E Fn A) \to E : A ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\}$
8	7	ffvelcdmda	$⊢ ((G \in UHGraph \land E Fn A) \land F \in A) \to E (F) \in (𝒫 Vtx (G) ∖ \{\emptyset\})$
9	8	3impa	$⊢ (G \in UHGraph \land E Fn A \land F \in A) \to E (F) \in (𝒫 Vtx (G) ∖ \{\emptyset\})$
10		eldifsni	$⊢ E (F) \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \to E (F) \neq \emptyset$
11	9 10	syl	$⊢ (G \in UHGraph \land E Fn A \land F \in A) \to E (F) \neq \emptyset$

Metamath Proof Explorer