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 syl5eq 
 |-  ( ( ( 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 } ) ) )