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

Metamath Proof Explorer

Theorem vtxdginducedm1lem2

Description: Lemma 2 for vtxdginducedm1 : the domain of the edge function in the induced subgraph S of a pseudograph G obtained by removing one vertex N . (Contributed by AV, 16-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdginducedm1.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
vtxdginducedm1.k ⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
vtxdginducedm1.i ⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
vtxdginducedm1.p ⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
vtxdginducedm1.s ⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
Assertion vtxdginducedm1lem2 dom ( iEdg ‘ 𝑆 ) = 𝐼

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdginducedm1.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 vtxdginducedm1.k ⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4 vtxdginducedm1.i ⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
5 vtxdginducedm1.p ⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
6 vtxdginducedm1.s ⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
7 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ ( iEdg ‘ 𝑆 ) = 𝑃
8 7 5 eqtri ⊢ ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐼 )
9 8 dmeqi ⊢ dom ( iEdg ‘ 𝑆 ) = dom ( 𝐸 ↾ 𝐼 )
10 4 ssrab3 ⊢ 𝐼 ⊆ dom 𝐸
11 ssdmres ⊢ ( 𝐼 ⊆ dom 𝐸 ↔ dom ( 𝐸 ↾ 𝐼 ) = 𝐼 )
12 10 11 mpbi ⊢ dom ( 𝐸 ↾ 𝐼 ) = 𝐼
13 9 12 eqtri ⊢ dom ( iEdg ‘ 𝑆 ) = 𝐼