Metamath Proof Explorer

Theorem upgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 ) is a pseudograph. (Contributed by AV, 8-Nov-2020) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v ⊢ V = Vtx ⁡ G
upgrres.e ⊢ E = iEdg ⁡ G
upgrres.f ⊢ F = i ∈ dom ⁡ E | N ∉ E ⁡ i
upgrres.s ⊢ S = V ∖ N E ↾ F
Assertion upgrres ⊢ G ∈ UPGraph ∧ N ∈ V → S ∈ UPGraph

Proof

Step Hyp Ref Expression
1 upgrres.v ⊢ V = Vtx ⁡ G
2 upgrres.e ⊢ E = iEdg ⁡ G
3 upgrres.f ⊢ F = i ∈ dom ⁡ E | N ∉ E ⁡ i
4 upgrres.s ⊢ S = V ∖ N E ↾ F
5 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
6 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
7 funres ⊢ Fun ⁡ E → Fun ⁡ E ↾ F
8 5 6 7 3syl ⊢ G ∈ UPGraph → Fun ⁡ E ↾ F
9 8 funfnd ⊢ G ∈ UPGraph → E ↾ F Fn dom ⁡ E ↾ F
10 9 adantr ⊢ G ∈ UPGraph ∧ N ∈ V → E ↾ F Fn dom ⁡ E ↾ F
11 1 2 3 upgrreslem ⊢ G ∈ UPGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
12 df-f ⊢ E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2 ↔ E ↾ F Fn dom ⁡ E ↾ F ∧ ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
13 10 11 12 sylanbrc ⊢ G ∈ UPGraph ∧ N ∈ V → E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
14 opex ⊢ V ∖ N E ↾ F ∈ V
15 4 14 eqeltri ⊢ S ∈ V
16 1 2 3 4 uhgrspan1lem2 ⊢ Vtx ⁡ S = V ∖ N
17 16 eqcomi ⊢ V ∖ N = Vtx ⁡ S
18 1 2 3 4 uhgrspan1lem3 ⊢ iEdg ⁡ S = E ↾ F
19 18 eqcomi ⊢ E ↾ F = iEdg ⁡ S
20 17 19 isupgr ⊢ S ∈ V → S ∈ UPGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
21 15 20 mp1i ⊢ G ∈ UPGraph ∧ N ∈ V → S ∈ UPGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
22 13 21 mpbird ⊢ G ∈ UPGraph ∧ N ∈ V → S ∈ UPGraph