Metamath Proof Explorer

Theorem umgredg

Description: For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses upgredg.v 
|- V = ( Vtx ` G )
upgredg.e 
|- E = ( Edg ` G )
Assertion umgredg 
|- ( ( G e. UMGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )

Proof

Step Hyp Ref Expression
1 upgredg.v 
 |-  V = ( Vtx ` G )
2 upgredg.e 
 |-  E = ( Edg ` G )
3 2 eleq2i 
 |-  ( C e. E <-> C e. ( Edg ` G ) )
4 edgumgr 
 |-  ( ( G e. UMGraph /\ C e. ( Edg ` G ) ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
5 3 4 sylan2b 
 |-  ( ( G e. UMGraph /\ C e. E ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
6 hash2prde 
 |-  ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> E. a E. b ( a =/= b /\ C = { a , b } ) )
7 eleq1 
 |-  ( C = { a , b } -> ( C e. ~P ( Vtx ` G ) <-> { a , b } e. ~P ( Vtx ` G ) ) )
8 prex 
 |-  { a , b } e. _V
9 8 elpw 
 |-  ( { a , b } e. ~P ( Vtx ` G ) <-> { a , b } C_ ( Vtx ` G ) )
10 vex 
 |-  a e. _V
11 vex 
 |-  b e. _V
12 10 11 prss 
 |-  ( ( a e. V /\ b e. V ) <-> { a , b } C_ V )
13 1 sseq2i 
 |-  ( { a , b } C_ V <-> { a , b } C_ ( Vtx ` G ) )
14 12 13 sylbbr 
 |-  ( { a , b } C_ ( Vtx ` G ) -> ( a e. V /\ b e. V ) )
15 9 14 sylbi 
 |-  ( { a , b } e. ~P ( Vtx ` G ) -> ( a e. V /\ b e. V ) )
16 7 15 syl6bi 
 |-  ( C = { a , b } -> ( C e. ~P ( Vtx ` G ) -> ( a e. V /\ b e. V ) ) )
17 16 adantrd 
 |-  ( C = { a , b } -> ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> ( a e. V /\ b e. V ) ) )
18 17 adantl 
 |-  ( ( a =/= b /\ C = { a , b } ) -> ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> ( a e. V /\ b e. V ) ) )
19 18 imdistanri 
 |-  ( ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) /\ ( a =/= b /\ C = { a , b } ) ) -> ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) )
20 19 ex 
 |-  ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> ( ( a =/= b /\ C = { a , b } ) -> ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) ) )
21 20 2eximdv 
 |-  ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> ( E. a E. b ( a =/= b /\ C = { a , b } ) -> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) ) )
22 6 21 mpd 
 |-  ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) )
23 5 22 syl 
 |-  ( ( G e. UMGraph /\ C e. E ) -> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) )
24 r2ex 
 |-  ( E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ C = { a , b } ) ) )
25 23 24 sylibr 
 |-  ( ( G e. UMGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )