Metamath Proof Explorer


Theorem uvtxupgrres

Description: A universal vertex is universal in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020)

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 uvtxupgrres
|- ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( K e. ( UnivVtx ` G ) -> K e. ( UnivVtx ` S ) ) )

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 1 uvtxnbgr
 |-  ( K e. ( UnivVtx ` G ) -> ( G NeighbVtx K ) = ( V \ { K } ) )
6 1 2 3 4 nbupgruvtxres
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) ) )
7 6 imp
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) )
8 difpr
 |-  ( V \ { N , K } ) = ( ( V \ { N } ) \ { K } )
9 1 2 3 4 upgrres1lem2
 |-  ( Vtx ` S ) = ( V \ { N } )
10 9 difeq1i
 |-  ( ( Vtx ` S ) \ { K } ) = ( ( V \ { N } ) \ { K } )
11 10 a1i
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( Vtx ` S ) \ { K } ) = ( ( V \ { N } ) \ { K } ) )
12 8 11 eqtr4id
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( V \ { N , K } ) = ( ( Vtx ` S ) \ { K } ) )
13 12 adantr
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( V \ { N , K } ) = ( ( Vtx ` S ) \ { K } ) )
14 7 13 eqtrd
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( S NeighbVtx K ) = ( ( Vtx ` S ) \ { K } ) )
15 simpr
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> K e. ( V \ { N } ) )
16 15 9 eleqtrrdi
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> K e. ( Vtx ` S ) )
17 16 adantr
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> K e. ( Vtx ` S ) )
18 eqid
 |-  ( Vtx ` S ) = ( Vtx ` S )
19 18 uvtxnbgrb
 |-  ( K e. ( Vtx ` S ) -> ( K e. ( UnivVtx ` S ) <-> ( S NeighbVtx K ) = ( ( Vtx ` S ) \ { K } ) ) )
20 17 19 syl
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> ( K e. ( UnivVtx ` S ) <-> ( S NeighbVtx K ) = ( ( Vtx ` S ) \ { K } ) ) )
21 14 20 mpbird
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) /\ ( G NeighbVtx K ) = ( V \ { K } ) ) -> K e. ( UnivVtx ` S ) )
22 21 ex
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( G NeighbVtx K ) = ( V \ { K } ) -> K e. ( UnivVtx ` S ) ) )
23 5 22 syl5
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( K e. ( UnivVtx ` G ) -> K e. ( UnivVtx ` S ) ) )