Metamath Proof Explorer


Theorem nbupgrres

Description: The neighborhood of a vertex in a restricted pseudograph (not necessarily valid for a hypergraph, because N , K and M could be connected by one edge, so M is a neighbor of K in the original graph, but not in the restricted graph, because the edge between M and K , also incident with N , was removed). (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020)

Ref Expression
Hypotheses nbupgrres.v
|- V = ( Vtx ` G )
nbupgrres.e
|- E = ( Edg ` G )
nbupgrres.f
|- F = { e e. E | N e/ e }
nbupgrres.s
|- S = <. ( V \ { N } ) , ( _I |` F ) >.
Assertion nbupgrres
|- ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( G NeighbVtx K ) -> M e. ( S NeighbVtx K ) ) )

Proof

Step Hyp Ref Expression
1 nbupgrres.v
 |-  V = ( Vtx ` G )
2 nbupgrres.e
 |-  E = ( Edg ` G )
3 nbupgrres.f
 |-  F = { e e. E | N e/ e }
4 nbupgrres.s
 |-  S = <. ( V \ { N } ) , ( _I |` F ) >.
5 simp1l
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> G e. UPGraph )
6 eldifi
 |-  ( K e. ( V \ { N } ) -> K e. V )
7 6 3ad2ant2
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> K e. V )
8 eldifsn
 |-  ( M e. ( ( V \ { N } ) \ { K } ) <-> ( M e. ( V \ { N } ) /\ M =/= K ) )
9 eldifi
 |-  ( M e. ( V \ { N } ) -> M e. V )
10 9 anim1i
 |-  ( ( M e. ( V \ { N } ) /\ M =/= K ) -> ( M e. V /\ M =/= K ) )
11 8 10 sylbi
 |-  ( M e. ( ( V \ { N } ) \ { K } ) -> ( M e. V /\ M =/= K ) )
12 difpr
 |-  ( V \ { N , K } ) = ( ( V \ { N } ) \ { K } )
13 11 12 eleq2s
 |-  ( M e. ( V \ { N , K } ) -> ( M e. V /\ M =/= K ) )
14 13 3ad2ant3
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. V /\ M =/= K ) )
15 1 2 nbupgrel
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( M e. V /\ M =/= K ) ) -> ( M e. ( G NeighbVtx K ) <-> { M , K } e. E ) )
16 5 7 14 15 syl21anc
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( G NeighbVtx K ) <-> { M , K } e. E ) )
17 16 biimpa
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> { M , K } e. E )
18 12 eleq2i
 |-  ( M e. ( V \ { N , K } ) <-> M e. ( ( V \ { N } ) \ { K } ) )
19 eldifsn
 |-  ( M e. ( V \ { N } ) <-> ( M e. V /\ M =/= N ) )
20 19 anbi1i
 |-  ( ( M e. ( V \ { N } ) /\ M =/= K ) <-> ( ( M e. V /\ M =/= N ) /\ M =/= K ) )
21 18 8 20 3bitri
 |-  ( M e. ( V \ { N , K } ) <-> ( ( M e. V /\ M =/= N ) /\ M =/= K ) )
22 simpr
 |-  ( ( M e. V /\ M =/= N ) -> M =/= N )
23 22 necomd
 |-  ( ( M e. V /\ M =/= N ) -> N =/= M )
24 23 adantr
 |-  ( ( ( M e. V /\ M =/= N ) /\ M =/= K ) -> N =/= M )
25 21 24 sylbi
 |-  ( M e. ( V \ { N , K } ) -> N =/= M )
26 25 3ad2ant3
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> N =/= M )
27 eldifsn
 |-  ( K e. ( V \ { N } ) <-> ( K e. V /\ K =/= N ) )
28 simpr
 |-  ( ( K e. V /\ K =/= N ) -> K =/= N )
29 28 necomd
 |-  ( ( K e. V /\ K =/= N ) -> N =/= K )
30 27 29 sylbi
 |-  ( K e. ( V \ { N } ) -> N =/= K )
31 30 3ad2ant2
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> N =/= K )
32 26 31 nelprd
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> -. N e. { M , K } )
33 df-nel
 |-  ( N e/ { M , K } <-> -. N e. { M , K } )
34 32 33 sylibr
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> N e/ { M , K } )
35 34 adantr
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> N e/ { M , K } )
36 neleq2
 |-  ( e = { M , K } -> ( N e/ e <-> N e/ { M , K } ) )
37 36 3 elrab2
 |-  ( { M , K } e. F <-> ( { M , K } e. E /\ N e/ { M , K } ) )
38 17 35 37 sylanbrc
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> { M , K } e. F )
39 1 2 3 4 upgrres1
 |-  ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph )
40 39 3ad2ant1
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> S e. UPGraph )
41 simp2
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> K e. ( V \ { N } ) )
42 18 8 sylbb
 |-  ( M e. ( V \ { N , K } ) -> ( M e. ( V \ { N } ) /\ M =/= K ) )
43 42 3ad2ant3
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( V \ { N } ) /\ M =/= K ) )
44 40 41 43 jca31
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( ( S e. UPGraph /\ K e. ( V \ { N } ) ) /\ ( M e. ( V \ { N } ) /\ M =/= K ) ) )
45 44 adantr
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> ( ( S e. UPGraph /\ K e. ( V \ { N } ) ) /\ ( M e. ( V \ { N } ) /\ M =/= K ) ) )
46 1 2 3 4 upgrres1lem2
 |-  ( Vtx ` S ) = ( V \ { N } )
47 46 eqcomi
 |-  ( V \ { N } ) = ( Vtx ` S )
48 edgval
 |-  ( Edg ` S ) = ran ( iEdg ` S )
49 1 2 3 4 upgrres1lem3
 |-  ( iEdg ` S ) = ( _I |` F )
50 49 rneqi
 |-  ran ( iEdg ` S ) = ran ( _I |` F )
51 rnresi
 |-  ran ( _I |` F ) = F
52 48 50 51 3eqtrri
 |-  F = ( Edg ` S )
53 47 52 nbupgrel
 |-  ( ( ( S e. UPGraph /\ K e. ( V \ { N } ) ) /\ ( M e. ( V \ { N } ) /\ M =/= K ) ) -> ( M e. ( S NeighbVtx K ) <-> { M , K } e. F ) )
54 45 53 syl
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> ( M e. ( S NeighbVtx K ) <-> { M , K } e. F ) )
55 38 54 mpbird
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) /\ M e. ( G NeighbVtx K ) ) -> M e. ( S NeighbVtx K ) )
56 55 ex
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( G NeighbVtx K ) -> M e. ( S NeighbVtx K ) ) )