upgrle2

Description: An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021)

		Ref	Expression
	Hypothesis	upgrle2.i	$⊢ I = iEdg (G)$
	Assertion	upgrle2	$⊢ (G \in UPGraph \land X \in dom I) \to \|I (X)\| \leq 2$

Step	Hyp	Ref	Expression
1		upgrle2.i	$⊢ I = iEdg (G)$
2		simpl	$⊢ (G \in UPGraph \land X \in dom I) \to G \in UPGraph$
3		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
4	1	uhgrfun	$⊢ G \in UHGraph \to Fun I$
5	3 4	syl	$⊢ G \in UPGraph \to Fun I$
6	5	funfnd	$⊢ G \in UPGraph \to I Fn dom I$
7	6	adantr	$⊢ (G \in UPGraph \land X \in dom I) \to I Fn dom I$
8		simpr	$⊢ (G \in UPGraph \land X \in dom I) \to X \in dom I$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9 1	upgrle	$⊢ (G \in UPGraph \land I Fn dom I \land X \in dom I) \to \|I (X)\| \leq 2$
11	2 7 8 10	syl3anc	$⊢ (G \in UPGraph \land X \in dom I) \to \|I (X)\| \leq 2$

Metamath Proof Explorer