This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )