Metamath Proof Explorer

Theorem usgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 ) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (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 usgrres ⊢ G ∈ USGraph ∧ N ∈ V → S ∈ USGraph

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 1 2 usgrf ⊢ G ∈ USGraph → E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 V ∖ ∅ | x = 2
6 3 ssrab3 ⊢ F ⊆ dom ⁡ E
7 6 a1i ⊢ G ∈ USGraph ∧ N ∈ V → F ⊆ dom ⁡ E
8 f1ssres ⊢ E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 V ∖ ∅ | x = 2 ∧ F ⊆ dom ⁡ E → E ↾ F : F ⟶ 1-1 x ∈ 𝒫 V ∖ ∅ | x = 2
9 5 7 8 syl2an2r ⊢ G ∈ USGraph ∧ N ∈ V → E ↾ F : F ⟶ 1-1 x ∈ 𝒫 V ∖ ∅ | x = 2
10 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
11 1 2 3 umgrreslem ⊢ G ∈ UMGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2
12 10 11 sylan ⊢ G ∈ USGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2
13 f1ssr ⊢ E ↾ F : F ⟶ 1-1 x ∈ 𝒫 V ∖ ∅ | x = 2 ∧ ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2 → E ↾ F : F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
14 9 12 13 syl2anc ⊢ G ∈ USGraph ∧ N ∈ V → E ↾ F : F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
15 ssdmres ⊢ F ⊆ dom ⁡ E ↔ dom ⁡ E ↾ F = F
16 6 15 mpbi ⊢ dom ⁡ E ↾ F = F
17 f1eq2 ⊢ dom ⁡ E ↾ F = F → E ↾ F : dom ⁡ E ↾ F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2 ↔ E ↾ F : F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
18 16 17 ax-mp ⊢ E ↾ F : dom ⁡ E ↾ F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2 ↔ E ↾ F : F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
19 14 18 sylibr ⊢ G ∈ USGraph ∧ N ∈ V → E ↾ F : dom ⁡ E ↾ F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
20 opex ⊢ V ∖ N E ↾ F ∈ V
21 4 20 eqeltri ⊢ S ∈ V
22 1 2 3 4 uhgrspan1lem2 ⊢ Vtx ⁡ S = V ∖ N
23 22 eqcomi ⊢ V ∖ N = Vtx ⁡ S
24 1 2 3 4 uhgrspan1lem3 ⊢ iEdg ⁡ S = E ↾ F
25 24 eqcomi ⊢ E ↾ F = iEdg ⁡ S
26 23 25 isusgrs ⊢ S ∈ V → S ∈ USGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
27 21 26 mp1i ⊢ G ∈ USGraph ∧ N ∈ V → S ∈ USGraph ↔ E ↾ F : dom ⁡ E ↾ F ⟶ 1-1 p ∈ 𝒫 V ∖ N | p = 2
28 19 27 mpbird ⊢ G ∈ USGraph ∧ N ∈ V → S ∈ USGraph