Metamath Proof Explorer

Theorem umgr2edgneu

Description: If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 . Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 9-Jan-2020)

Ref Expression
Hypothesis umgrvad2edg.e 
|- E = ( Edg ` G )
Assertion umgr2edgneu 
|- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. E N e. x )

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e 
 |-  E = ( Edg ` G )
2 1 umgrvad2edg 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
3 3simpc 
 |-  ( ( x =/= y /\ N e. x /\ N e. y ) -> ( N e. x /\ N e. y ) )
4 neneq 
 |-  ( x =/= y -> -. x = y )
5 4 3ad2ant1 
 |-  ( ( x =/= y /\ N e. x /\ N e. y ) -> -. x = y )
6 3 5 jca 
 |-  ( ( x =/= y /\ N e. x /\ N e. y ) -> ( ( N e. x /\ N e. y ) /\ -. x = y ) )
7 6 reximi 
 |-  ( E. y e. E ( x =/= y /\ N e. x /\ N e. y ) -> E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) )
8 7 reximi 
 |-  ( E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) -> E. x e. E E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) )
9 2 8 syl 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. E E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) )
10 rexanali 
 |-  ( E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) <-> -. A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) )
11 10 rexbii 
 |-  ( E. x e. E E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) <-> E. x e. E -. A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) )
12 rexnal 
 |-  ( E. x e. E -. A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) <-> -. A. x e. E A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) )
13 11 12 bitri 
 |-  ( E. x e. E E. y e. E ( ( N e. x /\ N e. y ) /\ -. x = y ) <-> -. A. x e. E A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) )
14 9 13 sylib 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. A. x e. E A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) )
15 14 intnand 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. ( E. x e. E N e. x /\ A. x e. E A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) ) )
16 eleq2w 
 |-  ( x = y -> ( N e. x <-> N e. y ) )
17 16 reu4 
 |-  ( E! x e. E N e. x <-> ( E. x e. E N e. x /\ A. x e. E A. y e. E ( ( N e. x /\ N e. y ) -> x = y ) ) )
18 15 17 sylnibr 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. E N e. x )