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 ‘ 𝑆 ) = 𝐼