Metamath Proof Explorer

Theorem uspgr1v1eop

Description: A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 dfsn2 
 |-  { B } = { B , B }
2 1 opeq2i 
 |-  <. A , { B } >. = <. A , { B , B } >.
3 2 sneqi 
 |-  { <. A , { B } >. } = { <. A , { B , B } >. }
4 3 opeq2i 
 |-  <. V , { <. A , { B } >. } >. = <. V , { <. A , { B , B } >. } >.
5 3simpa 
 |-  ( ( V e. W /\ A e. X /\ B e. V ) -> ( V e. W /\ A e. X ) )
6 id 
 |-  ( B e. V -> B e. V )
7 6 ancri 
 |-  ( B e. V -> ( B e. V /\ B e. V ) )
8 7 3ad2ant3 
 |-  ( ( V e. W /\ A e. X /\ B e. V ) -> ( B e. V /\ B e. V ) )
9 uspgr1eop 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ B e. V ) ) -> <. V , { <. A , { B , B } >. } >. e. USPGraph )
10 5 8 9 syl2anc 
 |-  ( ( V e. W /\ A e. X /\ B e. V ) -> <. V , { <. A , { B , B } >. } >. e. USPGraph )
11 4 10 eqeltrid 
 |-  ( ( V e. W /\ A e. X /\ B e. V ) -> <. V , { <. A , { B } >. } >. e. USPGraph )