Theorem upgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 ) is a pseudograph. (Contributed by AV, 8-Nov-2020) (Revised by AV, 19-Dec-2021)

	Ref	Expression
Hypotheses	upgrres.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgrres.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	upgrres.f	⊢ 𝐹 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
	upgrres.s	⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸 ↾ 𝐹 ) ⟩
Assertion	upgrres	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UPGraph )

Proof

Step	Hyp	Ref	Expression
1		upgrres.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgrres.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		upgrres.f	⊢ 𝐹 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
4		upgrres.s	⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸 ↾ 𝐹 ) ⟩
5		upgruhgr	⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
6	2	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
7		funres	⊢ ( Fun 𝐸 → Fun ( 𝐸 ↾ 𝐹 ) )
8	5 6 7	3syl	⊢ ( 𝐺 ∈ UPGraph → Fun ( 𝐸 ↾ 𝐹 ) )
9	8	funfnd	⊢ ( 𝐺 ∈ UPGraph → ( 𝐸 ↾ 𝐹 ) Fn dom ( 𝐸 ↾ 𝐹 ) )
10	9	adantr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ↾ 𝐹 ) Fn dom ( 𝐸 ↾ 𝐹 ) )
11	1 2 3	upgrreslem	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( 𝐸 ↾ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
12		df-f	⊢ ( ( 𝐸 ↾ 𝐹 ) : dom ( 𝐸 ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ( ( 𝐸 ↾ 𝐹 ) Fn dom ( 𝐸 ↾ 𝐹 ) ∧ ran ( 𝐸 ↾ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
13	10 11 12	sylanbrc	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ↾ 𝐹 ) : dom ( 𝐸 ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
14		opex	⊢ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸 ↾ 𝐹 ) ⟩ ∈ V
15	4 14	eqeltri	⊢ 𝑆 ∈ V
16	1 2 3 4	uhgrspan1lem2	⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
17	16	eqcomi	⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
18	1 2 3 4	uhgrspan1lem3	⊢ ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐹 )
19	18	eqcomi	⊢ ( 𝐸 ↾ 𝐹 ) = ( iEdg ‘ 𝑆 )
20	17 19	isupgr	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ UPGraph ↔ ( 𝐸 ↾ 𝐹 ) : dom ( 𝐸 ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
21	15 20	mp1i	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑆 ∈ UPGraph ↔ ( 𝐸 ↾ 𝐹 ) : dom ( 𝐸 ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
22	13 21	mpbird	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UPGraph )