Metamath Proof Explorer


Theorem nbupgruvtxres

Description: The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 nbupgruvtxres.v
 |-  V = ( Vtx ` G )
2 nbupgruvtxres.e
 |-  E = ( Edg ` G )
3 nbupgruvtxres.f
 |-  F = { e e. E | N e/ e }
4 nbupgruvtxres.s
 |-  S = <. ( V \ { N } ) , ( _I |` F ) >.
5 eqid
 |-  ( Vtx ` S ) = ( Vtx ` S )
6 5 nbgrssovtx
 |-  ( S NeighbVtx K ) C_ ( ( Vtx ` S ) \ { K } )
7 difpr
 |-  ( V \ { N , K } ) = ( ( V \ { N } ) \ { K } )
8 1 2 3 4 upgrres1lem2
 |-  ( Vtx ` S ) = ( V \ { N } )
9 8 eqcomi
 |-  ( V \ { N } ) = ( Vtx ` S )
10 9 a1i
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( V \ { N } ) = ( Vtx ` S ) )
11 10 difeq1d
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( V \ { N } ) \ { K } ) = ( ( Vtx ` S ) \ { K } ) )
12 7 11 eqtrid
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( V \ { N , K } ) = ( ( Vtx ` S ) \ { K } ) )
13 6 12 sseqtrrid
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( S NeighbVtx K ) C_ ( V \ { N , K } ) )
14 13 adantr
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( S NeighbVtx K ) C_ ( V \ { N , K } ) )
15 simpl
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) )
16 15 anim1i
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) /\ n e. ( V \ { N , K } ) ) -> ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ n e. ( V \ { N , K } ) ) )
17 df-3an
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ n e. ( V \ { N , K } ) ) <-> ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ n e. ( V \ { N , K } ) ) )
18 16 17 sylibr
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) /\ n e. ( V \ { N , K } ) ) -> ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ n e. ( V \ { N , K } ) ) )
19 dif32
 |-  ( ( V \ { N } ) \ { K } ) = ( ( V \ { K } ) \ { N } )
20 7 19 eqtri
 |-  ( V \ { N , K } ) = ( ( V \ { K } ) \ { N } )
21 20 eleq2i
 |-  ( n e. ( V \ { N , K } ) <-> n e. ( ( V \ { K } ) \ { N } ) )
22 eldifsn
 |-  ( n e. ( ( V \ { K } ) \ { N } ) <-> ( n e. ( V \ { K } ) /\ n =/= N ) )
23 21 22 bitri
 |-  ( n e. ( V \ { N , K } ) <-> ( n e. ( V \ { K } ) /\ n =/= N ) )
24 23 simplbi
 |-  ( n e. ( V \ { N , K } ) -> n e. ( V \ { K } ) )
25 eleq2
 |-  ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( n e. ( G NeighbVtx K ) <-> n e. ( V \ { K } ) ) )
26 24 25 syl5ibr
 |-  ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( n e. ( V \ { N , K } ) -> n e. ( G NeighbVtx K ) ) )
27 26 adantl
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( n e. ( V \ { N , K } ) -> n e. ( G NeighbVtx K ) ) )
28 27 imp
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) /\ n e. ( V \ { N , K } ) ) -> n e. ( G NeighbVtx K ) )
29 1 2 3 4 nbupgrres
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ n e. ( V \ { N , K } ) ) -> ( n e. ( G NeighbVtx K ) -> n e. ( S NeighbVtx K ) ) )
30 18 28 29 sylc
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) /\ n e. ( V \ { N , K } ) ) -> n e. ( S NeighbVtx K ) )
31 14 30 eqelssd
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) )
32 31 ex
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) ) )