Metamath Proof Explorer

Theorem umgrvad2edg

Description: If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg . (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 9-Jan-2020) (Revised by AV, 8-Jun-2021)

Ref Expression
Hypothesis umgrvad2edg.e 
|- E = ( Edg ` G )
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 umgrvad2edg.e 
 |-  E = ( Edg ` G )
2 simpl 
 |-  ( ( { N , A } e. E /\ { B , N } e. E ) -> { N , A } e. E )
3 simpr 
 |-  ( ( { N , A } e. E /\ { B , N } e. E ) -> { B , N } e. E )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 1 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { N , A } e. E ) -> ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) )
6 5 ex 
 |-  ( G e. UMGraph -> ( { N , A } e. E -> ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) ) )
7 4 1 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { B , N } e. E ) -> ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
8 7 ex 
 |-  ( G e. UMGraph -> ( { B , N } e. E -> ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) )
9 6 8 anim12d 
 |-  ( G e. UMGraph -> ( ( { N , A } e. E /\ { B , N } e. E ) -> ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) ) )
10 9 adantr 
 |-  ( ( G e. UMGraph /\ A =/= B ) -> ( ( { N , A } e. E /\ { B , N } e. E ) -> ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) ) )
11 10 imp 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) )
12 simplr 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> A =/= B )
13 1 umgredgne 
 |-  ( ( G e. UMGraph /\ { N , A } e. E ) -> N =/= A )
14 13 necomd 
 |-  ( ( G e. UMGraph /\ { N , A } e. E ) -> A =/= N )
15 14 ad2ant2r 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> A =/= N )
16 12 15 jca 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( A =/= B /\ A =/= N ) )
17 16 olcd 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) )
18 prneimg 
 |-  ( ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) -> ( ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) -> { N , A } =/= { B , N } ) )
19 18 imp 
 |-  ( ( ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) /\ ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) ) -> { N , A } =/= { B , N } )
20 prid1g 
 |-  ( N e. ( Vtx ` G ) -> N e. { N , A } )
21 20 ad3antrrr 
 |-  ( ( ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) /\ ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) ) -> N e. { N , A } )
22 prid2g 
 |-  ( N e. ( Vtx ` G ) -> N e. { B , N } )
23 22 ad3antrrr 
 |-  ( ( ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) /\ ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) ) -> N e. { B , N } )
24 19 21 23 3jca 
 |-  ( ( ( ( N e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( B e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) /\ ( ( N =/= B /\ N =/= N ) \/ ( A =/= B /\ A =/= N ) ) ) -> ( { N , A } =/= { B , N } /\ N e. { N , A } /\ N e. { B , N } ) )
25 11 17 24 syl2anc 
 |-  ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( { N , A } =/= { B , N } /\ N e. { N , A } /\ N e. { B , N } ) )
26 neeq1 
 |-  ( x = { N , A } -> ( x =/= y <-> { N , A } =/= y ) )
27 eleq2 
 |-  ( x = { N , A } -> ( N e. x <-> N e. { N , A } ) )
28 26 27 3anbi12d 
 |-  ( x = { N , A } -> ( ( x =/= y /\ N e. x /\ N e. y ) <-> ( { N , A } =/= y /\ N e. { N , A } /\ N e. y ) ) )
29 neeq2 
 |-  ( y = { B , N } -> ( { N , A } =/= y <-> { N , A } =/= { B , N } ) )
30 eleq2 
 |-  ( y = { B , N } -> ( N e. y <-> N e. { B , N } ) )
31 29 30 3anbi13d 
 |-  ( y = { B , N } -> ( ( { N , A } =/= y /\ N e. { N , A } /\ N e. y ) <-> ( { N , A } =/= { B , N } /\ N e. { N , A } /\ N e. { B , N } ) ) )
32 28 31 rspc2ev 
 |-  ( ( { N , A } e. E /\ { B , N } e. E /\ ( { N , A } =/= { B , N } /\ N e. { N , A } /\ N e. { B , N } ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
33 2 3 25 32 syl2an23an 
 |-  ( ( ( 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 ) )