Metamath Proof Explorer

Theorem umgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 ) is a multigraph. (Contributed by AV, 27-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 umgrres ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph

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 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
6 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
7 funres ⊢ Fun ⁡ E → Fun ⁡ E ↾ F
8 5 6 7 3syl ⊢ G ∈ UMGraph → Fun ⁡ E ↾ F
9 8 funfnd ⊢ G ∈ UMGraph → E ↾ F Fn dom ⁡ E ↾ F
10 9 adantr ⊢ G ∈ UMGraph ∧ N ∈ V → E ↾ F Fn dom ⁡ E ↾ F
11 1 2 3 umgrreslem ⊢ G ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 isumgrs ⊢ S ∈ V → S ∈ UMGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N | p = 2
21 15 20 mp1i ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ p ∈ 𝒫 V ∖ N | p = 2
22 13 21 mpbird ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph