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