Theorem usgrres1

Description: Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted 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 Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020) (Proof shortened by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	upgrres1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgrres1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	upgrres1.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
	upgrres1.s	⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion	usgrres1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ USGraph )

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		f1of1	⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 –1-1→ 𝐹 )
7	5 6	mp1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : 𝐹 –1-1→ 𝐹 )
8		eqidd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) = ( I ↾ 𝐹 ) )
9		dmresi	⊢ dom ( I ↾ 𝐹 ) = 𝐹
10	9	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → dom ( I ↾ 𝐹 ) = 𝐹 )
11		eqidd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 = 𝐹 )
12	8 10 11	f1eq123d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ 𝐹 ↔ ( I ↾ 𝐹 ) : 𝐹 –1-1→ 𝐹 ) )
13	7 12	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ 𝐹 )
14		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
15	1 2 3	umgrres1lem	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
16	14 15	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
17		f1ssr	⊢ ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ 𝐹 ∧ ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
18	13 16 17	syl2anc	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
19		opex	⊢ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ∈ V
20	4 19	eqeltri	⊢ 𝑆 ∈ V
21	1 2 3 4	upgrres1lem2	⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
22	21	eqcomi	⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
23	1 2 3 4	upgrres1lem3	⊢ ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )
24	23	eqcomi	⊢ ( I ↾ 𝐹 ) = ( iEdg ‘ 𝑆 )
25	22 24	isusgrs	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ USGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
26	20 25	mp1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑆 ∈ USGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) –1-1→ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
27	18 26	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ USGraph )