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 ) ) )