Metamath Proof Explorer

Theorem umgr2v2enb1

Description: In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g 
|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
Assertion umgr2v2enb1 
|- ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( G NeighbVtx A ) = { B } )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g 
 |-  G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
2 1 umgr2v2e 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> G e. UMGraph )
3 1 umgr2v2evtxel 
 |-  ( ( V e. W /\ A e. V ) -> A e. ( Vtx ` G ) )
4 3 3adant3 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> A e. ( Vtx ` G ) )
5 4 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> A e. ( Vtx ` G ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
8 6 7 nbumgrvtx 
 |-  ( ( G e. UMGraph /\ A e. ( Vtx ` G ) ) -> ( G NeighbVtx A ) = { x e. ( Vtx ` G ) | { A , x } e. ( Edg ` G ) } )
9 2 5 8 syl2anc 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( G NeighbVtx A ) = { x e. ( Vtx ` G ) | { A , x } e. ( Edg ` G ) } )
10 1 umgr2v2eedg 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( Edg ` G ) = { { A , B } } )
11 10 eleq2d 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( { A , x } e. ( Edg ` G ) <-> { A , x } e. { { A , B } } ) )
12 11 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( { A , x } e. ( Edg ` G ) <-> { A , x } e. { { A , B } } ) )
13 12 adantr 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> ( { A , x } e. ( Edg ` G ) <-> { A , x } e. { { A , B } } ) )
14 prex 
 |-  { A , x } e. _V
15 14 elsn 
 |-  ( { A , x } e. { { A , B } } <-> { A , x } = { A , B } )
16 13 15 bitrdi 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> ( { A , x } e. ( Edg ` G ) <-> { A , x } = { A , B } ) )
17 simpr 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> x e. ( Vtx ` G ) )
18 simpll3 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> B e. V )
19 17 18 preq2b 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> ( { A , x } = { A , B } <-> x = B ) )
20 16 19 bitrd 
 |-  ( ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) /\ x e. ( Vtx ` G ) ) -> ( { A , x } e. ( Edg ` G ) <-> x = B ) )
21 20 pm5.32da 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( ( x e. ( Vtx ` G ) /\ { A , x } e. ( Edg ` G ) ) <-> ( x e. ( Vtx ` G ) /\ x = B ) ) )
22 1 umgr2v2evtx 
 |-  ( V e. W -> ( Vtx ` G ) = V )
23 22 3ad2ant1 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( Vtx ` G ) = V )
24 eleq12 
 |-  ( ( x = B /\ ( Vtx ` G ) = V ) -> ( x e. ( Vtx ` G ) <-> B e. V ) )
25 24 exbiri 
 |-  ( x = B -> ( ( Vtx ` G ) = V -> ( B e. V -> x e. ( Vtx ` G ) ) ) )
26 25 com13 
 |-  ( B e. V -> ( ( Vtx ` G ) = V -> ( x = B -> x e. ( Vtx ` G ) ) ) )
27 26 3ad2ant3 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( ( Vtx ` G ) = V -> ( x = B -> x e. ( Vtx ` G ) ) ) )
28 23 27 mpd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( x = B -> x e. ( Vtx ` G ) ) )
29 28 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( x = B -> x e. ( Vtx ` G ) ) )
30 29 pm4.71rd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( x = B <-> ( x e. ( Vtx ` G ) /\ x = B ) ) )
31 21 30 bitr4d 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( ( x e. ( Vtx ` G ) /\ { A , x } e. ( Edg ` G ) ) <-> x = B ) )
32 31 alrimiv 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> A. x ( ( x e. ( Vtx ` G ) /\ { A , x } e. ( Edg ` G ) ) <-> x = B ) )
33 rabeqsn 
 |-  ( { x e. ( Vtx ` G ) | { A , x } e. ( Edg ` G ) } = { B } <-> A. x ( ( x e. ( Vtx ` G ) /\ { A , x } e. ( Edg ` G ) ) <-> x = B ) )
34 32 33 sylibr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { x e. ( Vtx ` G ) | { A , x } e. ( Edg ` G ) } = { B } )
35 9 34 eqtrd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( G NeighbVtx A ) = { B } )