Theorem isusgrop

Description: The property of being an undirected simple graph 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, 30-Nov-2020)

	Ref	Expression
Assertion	isusgrop	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USGraph <-> 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	isusgrs	|- ( <. V , E >. e. _V -> ( <. V , E >. e. USGraph <-> ( 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. USGraph <-> ( 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	rabeqdv	|- ( ( V e. W /\ E e. X ) -> { p e. ~P ( Vtx ` <. V , E >. ) | ( # ` p ) = 2 } = { p e. ~P V | ( # ` p ) = 2 } )
11	6 7 10	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 } ) )
12	5 11	bitrd	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USGraph <-> E : dom E -1-1-> { p e. ~P V | ( # ` p ) = 2 } ) )