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