Theorem umgrupgr

Description: An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020)

	Ref	Expression
Assertion	umgrupgr	|- ( G e. UMGraph -> G e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
3	1 2	isumgr	|- ( G e. UMGraph -> ( G e. UMGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) )
4		id	|- ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
5		2re	|- 2 e. RR
6	5	leidi	|- 2 <_ 2
7	6	a1i	|- ( ( # ` x ) = 2 -> 2 <_ 2 )
8		breq1	|- ( ( # ` x ) = 2 -> ( ( # ` x ) <_ 2 <-> 2 <_ 2 ) )
9	7 8	mpbird	|- ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 )
10	9	a1i	|- ( x e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 ) )
11	10	ss2rabi	|- { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 }
12	11	a1i	|- ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
13	4 12	fssd	|- ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
14	3 13	syl6bi	|- ( G e. UMGraph -> ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
15	14	pm2.43i	|- ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
16	1 2	isupgr	|- ( G e. UMGraph -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
17	15 16	mpbird	|- ( G e. UMGraph -> G e. UPGraph )