Metamath Proof Explorer

Theorem umgrres1

Description: A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgrres1.v ⊢ V = Vtx ⁡ G
upgrres1.e ⊢ E = Edg ⁡ G
upgrres1.f ⊢ F = e ∈ E | N ∉ e
upgrres1.s ⊢ S = V ∖ N I ↾ F
Assertion umgrres1 ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph

Proof

Step Hyp Ref Expression
1 upgrres1.v ⊢ V = Vtx ⁡ G
2 upgrres1.e ⊢ E = Edg ⁡ G
3 upgrres1.f ⊢ F = e ∈ E | N ∉ e
4 upgrres1.s ⊢ S = V ∖ N I ↾ F
5 f1oi ⊢ I ↾ F : F ⟶ 1-1 onto F
6 f1of ⊢ I ↾ F : F ⟶ 1-1 onto F → I ↾ F : F ⟶ F
7 5 6 mp1i ⊢ G ∈ UMGraph ∧ N ∈ V → I ↾ F : F ⟶ F
8 7 ffdmd ⊢ G ∈ UMGraph ∧ N ∈ V → I ↾ F : dom ⁡ I ↾ F ⟶ F
9 rnresi ⊢ ran ⁡ I ↾ F = F
10 1 2 3 umgrres1lem ⊢ G ∈ UMGraph ∧ N ∈ V → ran ⁡ I ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2
11 9 10 eqsstrrid ⊢ G ∈ UMGraph ∧ N ∈ V → F ⊆ p ∈ 𝒫 V ∖ N | p = 2
12 8 11 fssd ⊢ G ∈ UMGraph ∧ N ∈ V → I ↾ F : dom ⁡ I ↾ F ⟶ p ∈ 𝒫 V ∖ N | p = 2
13 opex ⊢ V ∖ N I ↾ F ∈ V
14 4 13 eqeltri ⊢ S ∈ V
15 1 2 3 4 upgrres1lem2 ⊢ Vtx ⁡ S = V ∖ N
16 15 eqcomi ⊢ V ∖ N = Vtx ⁡ S
17 1 2 3 4 upgrres1lem3 ⊢ iEdg ⁡ S = I ↾ F
18 17 eqcomi ⊢ I ↾ F = iEdg ⁡ S
19 16 18 isumgrs ⊢ S ∈ V → S ∈ UMGraph ↔ I ↾ F : dom ⁡ I ↾ F ⟶ p ∈ 𝒫 V ∖ N | p = 2
20 14 19 mp1i ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph ↔ I ↾ F : dom ⁡ I ↾ F ⟶ p ∈ 𝒫 V ∖ N | p = 2
21 12 20 mpbird ⊢ G ∈ UMGraph ∧ N ∈ V → S ∈ UMGraph