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

Metamath Proof Explorer

Theorem usgredgreu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgredg3.v 
|- V = ( Vtx ` G )
usgredg3.e 
|- E = ( iEdg ` G )
Assertion usgredgreu 
|- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )

Proof

Step Hyp Ref Expression
1 usgredg3.v 
 |-  V = ( Vtx ` G )
2 usgredg3.e 
 |-  E = ( iEdg ` G )
3 1 2 usgredg4 
 |-  ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )
4 eqtr2 
 |-  ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> { Y , y } = { Y , x } )
5 vex 
 |-  y e. _V
6 vex 
 |-  x e. _V
7 5 6 preqr2 
 |-  ( { Y , y } = { Y , x } -> y = x )
8 4 7 syl 
 |-  ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x )
9 8 a1i 
 |-  ( ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) /\ ( y e. V /\ x e. V ) ) -> ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) )
10 9 ralrimivva 
 |-  ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> A. y e. V A. x e. V ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) )
11 preq2 
 |-  ( y = x -> { Y , y } = { Y , x } )
12 11 eqeq2d 
 |-  ( y = x -> ( ( E ` X ) = { Y , y } <-> ( E ` X ) = { Y , x } ) )
13 12 reu4 
 |-  ( E! y e. V ( E ` X ) = { Y , y } <-> ( E. y e. V ( E ` X ) = { Y , y } /\ A. y e. V A. x e. V ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) ) )
14 3 10 13 sylanbrc 
 |-  ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )