Metamath Proof Explorer

Theorem usgr1eop

Description: A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = ( Vtx ` <. V , { <. A , { B , C } >. } >. )
2 simpllr 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> A e. X )
3 simplrl 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B e. V )
4 simpl 
 |-  ( ( V e. W /\ A e. X ) -> V e. W )
5 4 adantr 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> V e. W )
6 snex 
 |-  { <. A , { B , C } >. } e. _V
7 6 a1i 
 |-  ( B =/= C -> { <. A , { B , C } >. } e. _V )
8 opvtxfv 
 |-  ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
9 5 7 8 syl2an 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
10 3 9 eleqtrrd 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
11 simprr 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. V )
12 6 a1i 
 |-  ( ( B e. V /\ C e. V ) -> { <. A , { B , C } >. } e. _V )
13 4 12 8 syl2an 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
14 11 13 eleqtrrd 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
15 14 adantr 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
16 opiedgfv 
 |-  ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
17 5 7 16 syl2an 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
18 simpr 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B =/= C )
19 1 2 10 15 17 18 usgr1e 
 |-  ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> <. V , { <. A , { B , C } >. } >. e. USGraph )
20 19 ex 
 |-  ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( B =/= C -> <. V , { <. A , { B , C } >. } >. e. USGraph ) )