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