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

Metamath Proof Explorer

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