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