Metamath Proof Explorer

Theorem uspgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 6-Dec-2020)

Ref Expression
Assertion uspgredg2vtxeu 
|- ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E! y e. ( Vtx ` G ) E = { Y , y } )

Proof

Step Hyp Ref Expression
1 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 2 3 upgredg2vtx 
 |-  ( ( G e. UPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E. y e. ( Vtx ` G ) E = { Y , y } )
5 1 4 syl3an1 
 |-  ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E. y e. ( Vtx ` G ) E = { Y , y } )
6 eqtr2 
 |-  ( ( E = { Y , y } /\ E = { Y , x } ) -> { Y , y } = { Y , x } )
7 vex 
 |-  y e. _V
8 vex 
 |-  x e. _V
9 7 8 preqr2 
 |-  ( { Y , y } = { Y , x } -> y = x )
10 6 9 syl 
 |-  ( ( E = { Y , y } /\ E = { Y , x } ) -> y = x )
11 10 a1i 
 |-  ( ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) /\ ( y e. ( Vtx ` G ) /\ x e. ( Vtx ` G ) ) ) -> ( ( E = { Y , y } /\ E = { Y , x } ) -> y = x ) )
12 11 ralrimivva 
 |-  ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> A. y e. ( Vtx ` G ) A. x e. ( Vtx ` G ) ( ( E = { Y , y } /\ E = { Y , x } ) -> y = x ) )
13 preq2 
 |-  ( y = x -> { Y , y } = { Y , x } )
14 13 eqeq2d 
 |-  ( y = x -> ( E = { Y , y } <-> E = { Y , x } ) )
15 14 reu4 
 |-  ( E! y e. ( Vtx ` G ) E = { Y , y } <-> ( E. y e. ( Vtx ` G ) E = { Y , y } /\ A. y e. ( Vtx ` G ) A. x e. ( Vtx ` G ) ( ( E = { Y , y } /\ E = { Y , x } ) -> y = x ) ) )
16 5 12 15 sylanbrc 
 |-  ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E! y e. ( Vtx ` G ) E = { Y , y } )