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

Metamath Proof Explorer

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 } ) )