# 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 𝑉 = ( Vtx ‘ 𝐺 )
upgrres.e 𝐸 = ( iEdg ‘ 𝐺 )
upgrres.f 𝐹 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
upgrres.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩
Assertion usgrres ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → 𝑆 ∈ USGraph )

### Proof

Step Hyp Ref Expression
1 upgrres.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgrres.e 𝐸 = ( iEdg ‘ 𝐺 )
3 upgrres.f 𝐹 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
4 upgrres.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩
5 1 2 usgrf ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 3 ssrab3 𝐹 ⊆ dom 𝐸
7 6 a1i ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → 𝐹 ⊆ dom 𝐸 )
8 f1ssres ( ( 𝐸 : dom 𝐸1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ 𝐹 ⊆ dom 𝐸 ) → ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
9 5 7 8 syl2an2r ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
10 usgrumgr ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
11 1 2 3 umgrreslem ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → ran ( 𝐸𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
12 10 11 sylan ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ran ( 𝐸𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
13 f1ssr ( ( ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ran ( 𝐸𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) → ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
14 9 12 13 syl2anc ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
15 ssdmres ( 𝐹 ⊆ dom 𝐸 ↔ dom ( 𝐸𝐹 ) = 𝐹 )
16 6 15 mpbi dom ( 𝐸𝐹 ) = 𝐹
17 f1eq2 ( dom ( 𝐸𝐹 ) = 𝐹 → ( ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
18 16 17 ax-mp ( ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( 𝐸𝐹 ) : 𝐹1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
19 14 18 sylibr ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
20 opex ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩ ∈ V
21 4 20 eqeltri 𝑆 ∈ V
22 1 2 3 4 uhgrspan1lem2 ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
23 22 eqcomi ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
24 1 2 3 4 uhgrspan1lem3 ( iEdg ‘ 𝑆 ) = ( 𝐸𝐹 )
25 24 eqcomi ( 𝐸𝐹 ) = ( iEdg ‘ 𝑆 )
26 23 25 isusgrs ( 𝑆 ∈ V → ( 𝑆 ∈ USGraph ↔ ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
27 21 26 mp1i ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ( 𝑆 ∈ USGraph ↔ ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
28 19 27 mpbird ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → 𝑆 ∈ USGraph )