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 | N e
nbupgruvtxres.s S = V N I F
Assertion uvtxupgrres G UPGraph N V K V N K UnivVtx G K 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 | N e
4 nbupgruvtxres.s S = V N I F
5 1 uvtxnbgr K UnivVtx G G NeighbVtx K = V K
6 1 2 3 4 nbupgruvtxres G UPGraph N V K V N G NeighbVtx K = V K S NeighbVtx K = V N K
7 6 imp G UPGraph N V K 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 UPGraph N V K V N Vtx S K = V N K
12 8 11 eqtr4id G UPGraph N V K V N V N K = Vtx S K
13 12 adantr G UPGraph N V K V N G NeighbVtx K = V K V N K = Vtx S K
14 7 13 eqtrd G UPGraph N V K V N G NeighbVtx K = V K S NeighbVtx K = Vtx S K
15 simpr G UPGraph N V K V N K V N
16 15 9 eleqtrrdi G UPGraph N V K V N K Vtx S
17 16 adantr G UPGraph N V K V N G NeighbVtx K = V K K Vtx S
18 eqid Vtx S = Vtx S
19 18 uvtxnbgrb K Vtx S K UnivVtx S S NeighbVtx K = Vtx S K
20 17 19 syl G UPGraph N V K V N G NeighbVtx K = V K K UnivVtx S S NeighbVtx K = Vtx S K
21 14 20 mpbird G UPGraph N V K V N G NeighbVtx K = V K K UnivVtx S
22 21 ex G UPGraph N V K V N G NeighbVtx K = V K K UnivVtx S
23 5 22 syl5 G UPGraph N V K V N K UnivVtx G K UnivVtx S