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

Metamath Proof Explorer

Theorem usgr1e

Description: A simple graph with one edge (with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses uspgr1e.v 
|- V = ( Vtx ` G )
uspgr1e.a 
|- ( ph -> A e. X )
uspgr1e.b 
|- ( ph -> B e. V )
uspgr1e.c 
|- ( ph -> C e. V )
uspgr1e.e 
|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
usgr1e.e 
|- ( ph -> B =/= C )
Assertion usgr1e 
|- ( ph -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 uspgr1e.v 
 |-  V = ( Vtx ` G )
2 uspgr1e.a 
 |-  ( ph -> A e. X )
3 uspgr1e.b 
 |-  ( ph -> B e. V )
4 uspgr1e.c 
 |-  ( ph -> C e. V )
5 uspgr1e.e 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
6 usgr1e.e 
 |-  ( ph -> B =/= C )
7 1 2 3 4 5 uspgr1e 
 |-  ( ph -> G e. USPGraph )
8 hashprg 
 |-  ( ( B e. V /\ C e. V ) -> ( B =/= C <-> ( # ` { B , C } ) = 2 ) )
9 3 4 8 syl2anc 
 |-  ( ph -> ( B =/= C <-> ( # ` { B , C } ) = 2 ) )
10 6 9 mpbid 
 |-  ( ph -> ( # ` { B , C } ) = 2 )
11 prex 
 |-  { B , C } e. _V
12 fveqeq2 
 |-  ( x = { B , C } -> ( ( # ` x ) = 2 <-> ( # ` { B , C } ) = 2 ) )
13 11 12 ralsn 
 |-  ( A. x e. { { B , C } } ( # ` x ) = 2 <-> ( # ` { B , C } ) = 2 )
14 10 13 sylibr 
 |-  ( ph -> A. x e. { { B , C } } ( # ` x ) = 2 )
15 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
16 15 a1i 
 |-  ( ph -> ( Edg ` G ) = ran ( iEdg ` G ) )
17 5 rneqd 
 |-  ( ph -> ran ( iEdg ` G ) = ran { <. A , { B , C } >. } )
18 rnsnopg 
 |-  ( A e. X -> ran { <. A , { B , C } >. } = { { B , C } } )
19 2 18 syl 
 |-  ( ph -> ran { <. A , { B , C } >. } = { { B , C } } )
20 16 17 19 3eqtrd 
 |-  ( ph -> ( Edg ` G ) = { { B , C } } )
21 14 20 raleqtrrdv 
 |-  ( ph -> A. x e. ( Edg ` G ) ( # ` x ) = 2 )
22 usgruspgrb 
 |-  ( G e. USGraph <-> ( G e. USPGraph /\ A. x e. ( Edg ` G ) ( # ` x ) = 2 ) )
23 7 21 22 sylanbrc 
 |-  ( ph -> G e. USGraph )