Theorem upgredg

Description: For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020) (Proof shortened by AV, 26-Nov-2021)

	Ref	Expression
Hypotheses	upgredg.v	|- V = ( Vtx ` G )
	upgredg.e	|- E = ( Edg ` G )
Assertion	upgredg	|- ( ( G e. UPGraph /\ C e. E ) -> E. a e. V E. b e. V C = { a , b } )

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	|- V = ( Vtx ` G )
2		upgredg.e	|- E = ( Edg ` G )
3		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
4	3	a1i	|- ( G e. UPGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
5	2 4	eqtrid	|- ( G e. UPGraph -> E = ran ( iEdg ` G ) )
6	5	eleq2d	|- ( G e. UPGraph -> ( C e. E <-> C e. ran ( iEdg ` G ) ) )
7		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
8	1 7	upgrf	|- ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
9	8	frnd	|- ( G e. UPGraph -> ran ( iEdg ` G ) C_ { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
10	9	sseld	|- ( G e. UPGraph -> ( C e. ran ( iEdg ` G ) -> C e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
11	6 10	sylbid	|- ( G e. UPGraph -> ( C e. E -> C e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
12	11	imp	|- ( ( G e. UPGraph /\ C e. E ) -> C e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
13		fveq2	|- ( x = C -> ( # ` x ) = ( # ` C ) )
14	13	breq1d	|- ( x = C -> ( ( # ` x ) <_ 2 <-> ( # ` C ) <_ 2 ) )
15	14	elrab	|- ( C e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( C e. ( ~P V \ { (/) } ) /\ ( # ` C ) <_ 2 ) )
16		hashle2prv	|- ( C e. ( ~P V \ { (/) } ) -> ( ( # ` C ) <_ 2 <-> E. a e. V E. b e. V C = { a , b } ) )
17	16	biimpa	|- ( ( C e. ( ~P V \ { (/) } ) /\ ( # ` C ) <_ 2 ) -> E. a e. V E. b e. V C = { a , b } )
18	15 17	sylbi	|- ( C e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> E. a e. V E. b e. V C = { a , b } )
19	12 18	syl	|- ( ( G e. UPGraph /\ C e. E ) -> E. a e. V E. b e. V C = { a , b } )