Metamath Proof Explorer

Theorem usgredg4

Description: For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

Ref Expression
Hypotheses usgredg3.v 
|- V = ( Vtx ` G )
usgredg3.e 
|- E = ( iEdg ` G )
Assertion usgredg4 
|- ( ( 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 usgredg3 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> E. x e. V E. z e. V ( x =/= z /\ ( E ` X ) = { x , z } ) )
4 eleq2 
 |-  ( ( E ` X ) = { x , z } -> ( Y e. ( E ` X ) <-> Y e. { x , z } ) )
5 4 adantl 
 |-  ( ( x =/= z /\ ( E ` X ) = { x , z } ) -> ( Y e. ( E ` X ) <-> Y e. { x , z } ) )
6 5 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> ( Y e. ( E ` X ) <-> Y e. { x , z } ) )
7 simplrr 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> z e. V )
8 7 adantl 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> z e. V )
9 preq2 
 |-  ( y = z -> { x , y } = { x , z } )
10 9 eqeq2d 
 |-  ( y = z -> ( { x , z } = { x , y } <-> { x , z } = { x , z } ) )
11 10 adantl 
 |-  ( ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) /\ y = z ) -> ( { x , z } = { x , y } <-> { x , z } = { x , z } ) )
12 eqidd 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> { x , z } = { x , z } )
13 8 11 12 rspcedvd 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> E. y e. V { x , z } = { x , y } )
14 simprr 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> ( E ` X ) = { x , z } )
15 preq1 
 |-  ( Y = x -> { Y , y } = { x , y } )
16 14 15 eqeqan12rd 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> ( ( E ` X ) = { Y , y } <-> { x , z } = { x , y } ) )
17 16 rexbidv 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> ( E. y e. V ( E ` X ) = { Y , y } <-> E. y e. V { x , z } = { x , y } ) )
18 13 17 mpbird 
 |-  ( ( Y = x /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> E. y e. V ( E ` X ) = { Y , y } )
19 18 ex 
 |-  ( Y = x -> ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> E. y e. V ( E ` X ) = { Y , y } ) )
20 simplrl 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> x e. V )
21 20 adantl 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> x e. V )
22 preq2 
 |-  ( y = x -> { z , y } = { z , x } )
23 22 eqeq2d 
 |-  ( y = x -> ( { x , z } = { z , y } <-> { x , z } = { z , x } ) )
24 23 adantl 
 |-  ( ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) /\ y = x ) -> ( { x , z } = { z , y } <-> { x , z } = { z , x } ) )
25 prcom 
 |-  { x , z } = { z , x }
26 25 a1i 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> { x , z } = { z , x } )
27 21 24 26 rspcedvd 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> E. y e. V { x , z } = { z , y } )
28 preq1 
 |-  ( Y = z -> { Y , y } = { z , y } )
29 14 28 eqeqan12rd 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> ( ( E ` X ) = { Y , y } <-> { x , z } = { z , y } ) )
30 29 rexbidv 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> ( E. y e. V ( E ` X ) = { Y , y } <-> E. y e. V { x , z } = { z , y } ) )
31 27 30 mpbird 
 |-  ( ( Y = z /\ ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) ) -> E. y e. V ( E ` X ) = { Y , y } )
32 31 ex 
 |-  ( Y = z -> ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> E. y e. V ( E ` X ) = { Y , y } ) )
33 19 32 jaoi 
 |-  ( ( Y = x \/ Y = z ) -> ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> E. y e. V ( E ` X ) = { Y , y } ) )
34 elpri 
 |-  ( Y e. { x , z } -> ( Y = x \/ Y = z ) )
35 33 34 syl11 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> ( Y e. { x , z } -> E. y e. V ( E ` X ) = { Y , y } ) )
36 6 35 sylbid 
 |-  ( ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) /\ ( x =/= z /\ ( E ` X ) = { x , z } ) ) -> ( Y e. ( E ` X ) -> E. y e. V ( E ` X ) = { Y , y } ) )
37 36 ex 
 |-  ( ( ( G e. USGraph /\ X e. dom E ) /\ ( x e. V /\ z e. V ) ) -> ( ( x =/= z /\ ( E ` X ) = { x , z } ) -> ( Y e. ( E ` X ) -> E. y e. V ( E ` X ) = { Y , y } ) ) )
38 37 rexlimdvva 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E. x e. V E. z e. V ( x =/= z /\ ( E ` X ) = { x , z } ) -> ( Y e. ( E ` X ) -> E. y e. V ( E ` X ) = { Y , y } ) ) )
39 3 38 mpd 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( Y e. ( E ` X ) -> E. y e. V ( E ` X ) = { Y , y } ) )
40 39 3impia 
 |-  ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )