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	20	raleqdv	|- ( ph -> ( A. x e. ( Edg ` G ) ( # ` x ) = 2 <-> A. x e. { { B , C } } ( # ` x ) = 2 ) )
22	14 21	mpbird	|- ( ph -> A. x e. ( Edg ` G ) ( # ` x ) = 2 )
23		usgruspgrb	|- ( G e. USGraph <-> ( G e. USPGraph /\ A. x e. ( Edg ` G ) ( # ` x ) = 2 ) )
24	7 22 23	sylanbrc	|- ( ph -> G e. USGraph )