Metamath Proof Explorer

Theorem usgrexi

Description: An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 10-Nov-2021)

Ref Expression
Hypothesis usgrexi.p 
|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion usgrexi 
|- ( V e. W -> <. V , ( _I |` P ) >. e. USGraph )

Proof

Step Hyp Ref Expression
1 usgrexi.p 
 |-  P = { x e. ~P V | ( # ` x ) = 2 }
2 1 usgrexilem 
 |-  ( V e. W -> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
3 1 cusgrexilem1 
 |-  ( V e. W -> ( _I |` P ) e. _V )
4 opiedgfv 
 |-  ( ( V e. W /\ ( _I |` P ) e. _V ) -> ( iEdg ` <. V , ( _I |` P ) >. ) = ( _I |` P ) )
5 3 4 mpdan 
 |-  ( V e. W -> ( iEdg ` <. V , ( _I |` P ) >. ) = ( _I |` P ) )
6 5 dmeqd 
 |-  ( V e. W -> dom ( iEdg ` <. V , ( _I |` P ) >. ) = dom ( _I |` P ) )
7 opvtxfv 
 |-  ( ( V e. W /\ ( _I |` P ) e. _V ) -> ( Vtx ` <. V , ( _I |` P ) >. ) = V )
8 3 7 mpdan 
 |-  ( V e. W -> ( Vtx ` <. V , ( _I |` P ) >. ) = V )
9 8 pweqd 
 |-  ( V e. W -> ~P ( Vtx ` <. V , ( _I |` P ) >. ) = ~P V )
10 9 rabeqdv 
 |-  ( V e. W -> { x e. ~P ( Vtx ` <. V , ( _I |` P ) >. ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
11 5 6 10 f1eq123d 
 |-  ( V e. W -> ( ( iEdg ` <. V , ( _I |` P ) >. ) : dom ( iEdg ` <. V , ( _I |` P ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` P ) >. ) | ( # ` x ) = 2 } <-> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
12 2 11 mpbird 
 |-  ( V e. W -> ( iEdg ` <. V , ( _I |` P ) >. ) : dom ( iEdg ` <. V , ( _I |` P ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` P ) >. ) | ( # ` x ) = 2 } )
13 opex 
 |-  <. V , ( _I |` P ) >. e. _V
14 eqid 
 |-  ( Vtx ` <. V , ( _I |` P ) >. ) = ( Vtx ` <. V , ( _I |` P ) >. )
15 eqid 
 |-  ( iEdg ` <. V , ( _I |` P ) >. ) = ( iEdg ` <. V , ( _I |` P ) >. )
16 14 15 isusgrs 
 |-  ( <. V , ( _I |` P ) >. e. _V -> ( <. V , ( _I |` P ) >. e. USGraph <-> ( iEdg ` <. V , ( _I |` P ) >. ) : dom ( iEdg ` <. V , ( _I |` P ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` P ) >. ) | ( # ` x ) = 2 } ) )
17 13 16 mp1i 
 |-  ( V e. W -> ( <. V , ( _I |` P ) >. e. USGraph <-> ( iEdg ` <. V , ( _I |` P ) >. ) : dom ( iEdg ` <. V , ( _I |` P ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` P ) >. ) | ( # ` x ) = 2 } ) )
18 12 17 mpbird 
 |-  ( V e. W -> <. V , ( _I |` P ) >. e. USGraph )