This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )