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

Metamath Proof Explorer

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 } )