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 )