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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgrres1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	upgrres1.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
	upgrres1.s	⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion	umgrres1	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UMGraph )

Proof

Step	Hyp	Ref	Expression
1		upgrres1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgrres1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		upgrres1.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4		upgrres1.s	⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5		f1oi	⊢ ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹
6		f1of	⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
7	5 6	mp1i	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
8	7	ffdmd	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 )
9		rnresi	⊢ ran ( I ↾ 𝐹 ) = 𝐹
10	1 2 3	umgrres1lem	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
11	9 10	eqsstrrid	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
12	8 11	fssd	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
13		opex	⊢ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ∈ V
14	4 13	eqeltri	⊢ 𝑆 ∈ V
15	1 2 3 4	upgrres1lem2	⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
16	15	eqcomi	⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
17	1 2 3 4	upgrres1lem3	⊢ ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )
18	17	eqcomi	⊢ ( I ↾ 𝐹 ) = ( iEdg ‘ 𝑆 )
19	16 18	isumgrs	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ UMGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
20	14 19	mp1i	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑆 ∈ UMGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
21	12 20	mpbird	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UMGraph )