usgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Hypotheses	usgrf1o.e	$⊢ E = iEdg (G)$
	usgrss.v	$⊢ V = Vtx (G)$
Assertion	usgrss	$⊢ (G \in USGraph \land X \in dom E) \to E (X) \subseteq V$

Step	Hyp	Ref	Expression
1		usgrf1o.e	$⊢ E = iEdg (G)$
2		usgrss.v	$⊢ V = Vtx (G)$
3		ssrab2	$⊢ \{x \in 𝒫 V \| \|x\| = 2\} \subseteq 𝒫 V$
4	2 1	usgrfs	$⊢ G \in USGraph \to E : dom E \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$
5		f1f	$⊢ E : dom E \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \to E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$
6	4 5	syl	$⊢ G \in USGraph \to E : dom E ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$
7	6	ffvelcdmda	$⊢ (G \in USGraph \land X \in dom E) \to E (X) \in \{x \in 𝒫 V \| \|x\| = 2\}$
8	3 7	sselid	$⊢ (G \in USGraph \land X \in dom E) \to E (X) \in 𝒫 V$
9	8	elpwid	$⊢ (G \in USGraph \land X \in dom E) \to E (X) \subseteq V$

Metamath Proof Explorer