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

Step	Hyp	Ref	Expression
1		isupgr.v	$⊢ V = Vtx (G)$
2		isupgr.e	$⊢ E = iEdg (G)$
3		ssrab2	$⊢ \{x \in (𝒫 V ∖ \{\emptyset\}) \| \|x\| \leq 2\} \subseteq 𝒫 V ∖ \{\emptyset\}$
4	1 2	upgrfn	$⊢ (G \in UPGraph \land E Fn A) \to E : A ⟶ \{x \in (𝒫 V ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
5	4	ffvelcdmda	$⊢ ((G \in UPGraph \land E Fn A) \land F \in A) \to E (F) \in \{x \in (𝒫 V ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
6	5	3impa	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \in \{x \in (𝒫 V ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
7	3 6	sselid	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \in (𝒫 V ∖ \{\emptyset\})$
8		eldifsni	$⊢ E (F) \in (𝒫 V ∖ \{\emptyset\}) \to E (F) \neq \emptyset$
9	7 8	syl	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \neq \emptyset$

Metamath Proof Explorer