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

Metamath Proof Explorer

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 )