Theorem 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 e. UPGraph /\ X e. dom I ) -> ( # ` ( I ` X ) ) <_ 2 )

Proof

Step	Hyp	Ref	Expression
1		upgrle2.i	|- I = ( iEdg ` G )
2		simpl	|- ( ( G e. UPGraph /\ X e. dom I ) -> G e. UPGraph )
3		upgruhgr	|- ( G e. UPGraph -> G e. UHGraph )
4	1	uhgrfun	|- ( G e. UHGraph -> Fun I )
5	3 4	syl	|- ( G e. UPGraph -> Fun I )
6	5	funfnd	|- ( G e. UPGraph -> I Fn dom I )
7	6	adantr	|- ( ( G e. UPGraph /\ X e. dom I ) -> I Fn dom I )
8		simpr	|- ( ( G e. UPGraph /\ X e. dom I ) -> X e. dom I )
9		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
10	9 1	upgrle	|- ( ( G e. UPGraph /\ I Fn dom I /\ X e. dom I ) -> ( # ` ( I ` X ) ) <_ 2 )
11	2 7 8 10	syl3anc	|- ( ( G e. UPGraph /\ X e. dom I ) -> ( # ` ( I ` X ) ) <_ 2 )