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

Metamath Proof Explorer

Theorem uspgr1eop

Description: A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion uspgr1eop 
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. USPGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = ( Vtx ` <. V , { <. A , { B , C } >. } >. )
2 simplr 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> A e. X )
3 simprl 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> B e. V )
4 simpl 
 |-  ( ( V e. W /\ A e. X ) -> V e. W )
5 snex 
 |-  { <. A , { B , C } >. } e. _V
6 5 a1i 
 |-  ( ( B e. V /\ C e. V ) -> { <. A , { B , C } >. } e. _V )
7 opvtxfv 
 |-  ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
8 4 6 7 syl2an 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
9 3 8 eleqtrrd 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> B e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
10 simprr 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. V )
11 10 8 eleqtrrd 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
12 opiedgfv 
 |-  ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
13 4 6 12 syl2an 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
14 1 2 9 11 13 uspgr1e 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. USPGraph )