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 )