Theorem isuspgrop

Description: The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of Bollobas p. 1. (Contributed by AV, 25-Nov-2021)

	Ref	Expression
Assertion	isuspgrop	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USPGraph <-> E : dom E -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		opex	|- <. V , E >. e. _V
2		eqid	|- ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. )
3		eqid	|- ( iEdg ` <. V , E >. ) = ( iEdg ` <. V , E >. )
4	2 3	isuspgr	|- ( <. V , E >. e. _V -> ( <. V , E >. e. USPGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) -1-1-> { p e. ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
5	1 4	mp1i	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USPGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) -1-1-> { p e. ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
6		opiedgfv	|- ( ( V e. W /\ E e. X ) -> ( iEdg ` <. V , E >. ) = E )
7	6	dmeqd	|- ( ( V e. W /\ E e. X ) -> dom ( iEdg ` <. V , E >. ) = dom E )
8		opvtxfv	|- ( ( V e. W /\ E e. X ) -> ( Vtx ` <. V , E >. ) = V )
9	8	pweqd	|- ( ( V e. W /\ E e. X ) -> ~P ( Vtx ` <. V , E >. ) = ~P V )
10	9	difeq1d	|- ( ( V e. W /\ E e. X ) -> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) = ( ~P V \ { (/) } ) )
11	10	rabeqdv	|- ( ( V e. W /\ E e. X ) -> { p e. ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) | ( # ` p ) <_ 2 } = { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
12	6 7 11	f1eq123d	|- ( ( V e. W /\ E e. X ) -> ( ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) -1-1-> { p e. ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) | ( # ` p ) <_ 2 } <-> E : dom E -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
13	5 12	bitrd	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USPGraph <-> E : dom E -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )