Metamath Proof Explorer

Theorem umgr2edg1

Description: If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 8-Jun-2021)

Ref Expression
Hypotheses usgrf1oedg.i 
|- I = ( iEdg ` G )
usgrf1oedg.e 
|- E = ( Edg ` G )
Assertion umgr2edg1 
|- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. dom I N e. ( I ` x ) )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i 
 |-  I = ( iEdg ` G )
2 usgrf1oedg.e 
 |-  E = ( Edg ` G )
3 1 2 umgr2edg 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
4 3anrot 
 |-  ( ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) <-> ( N e. ( I ` x ) /\ N e. ( I ` y ) /\ x =/= y ) )
5 df-ne 
 |-  ( x =/= y <-> -. x = y )
6 5 3anbi3i 
 |-  ( ( N e. ( I ` x ) /\ N e. ( I ` y ) /\ x =/= y ) <-> ( N e. ( I ` x ) /\ N e. ( I ` y ) /\ -. x = y ) )
7 4 6 bitri 
 |-  ( ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) <-> ( N e. ( I ` x ) /\ N e. ( I ` y ) /\ -. x = y ) )
8 df-3an 
 |-  ( ( N e. ( I ` x ) /\ N e. ( I ` y ) /\ -. x = y ) <-> ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) )
9 7 8 bitri 
 |-  ( ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) <-> ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) )
10 9 2rexbii 
 |-  ( E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) <-> E. x e. dom I E. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) )
11 3 10 sylib 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) )
12 rexanali 
 |-  ( E. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) <-> -. A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) )
13 12 rexbii 
 |-  ( E. x e. dom I E. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) <-> E. x e. dom I -. A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) )
14 rexnal 
 |-  ( E. x e. dom I -. A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) <-> -. A. x e. dom I A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) )
15 13 14 bitri 
 |-  ( E. x e. dom I E. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) /\ -. x = y ) <-> -. A. x e. dom I A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) )
16 11 15 sylib 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. A. x e. dom I A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) )
17 16 intnand 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. ( E. x e. dom I N e. ( I ` x ) /\ A. x e. dom I A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) ) )
18 fveq2 
 |-  ( x = y -> ( I ` x ) = ( I ` y ) )
19 18 eleq2d 
 |-  ( x = y -> ( N e. ( I ` x ) <-> N e. ( I ` y ) ) )
20 19 reu4 
 |-  ( E! x e. dom I N e. ( I ` x ) <-> ( E. x e. dom I N e. ( I ` x ) /\ A. x e. dom I A. y e. dom I ( ( N e. ( I ` x ) /\ N e. ( I ` y ) ) -> x = y ) ) )
21 17 20 sylnibr 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. dom I N e. ( I ` x ) )