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 ⊢ V = Vtx ⁡ G
vtxdginducedm1.e ⊢ E = iEdg ⁡ G
vtxdginducedm1.k ⊢ K = V ∖ N
vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
vtxdginducedm1.p ⊢ P = E ↾ I
vtxdginducedm1.s ⊢ S = K P
Assertion vtxdginducedm1lem2 ⊢ dom ⁡ iEdg ⁡ S = I

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ⊢ V = Vtx ⁡ G
2 vtxdginducedm1.e ⊢ E = iEdg ⁡ G
3 vtxdginducedm1.k ⊢ K = V ∖ N
4 vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
5 vtxdginducedm1.p ⊢ P = E ↾ I
6 vtxdginducedm1.s ⊢ S = K P
7 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ iEdg ⁡ S = P
8 7 5 eqtri ⊢ iEdg ⁡ S = E ↾ I
9 8 dmeqi ⊢ dom ⁡ iEdg ⁡ S = dom ⁡ E ↾ I
10 4 ssrab3 ⊢ I ⊆ dom ⁡ E
11 ssdmres ⊢ I ⊆ dom ⁡ E ↔ dom ⁡ E ↾ I = I
12 10 11 mpbi ⊢ dom ⁡ E ↾ I = I
13 9 12 eqtri ⊢ dom ⁡ iEdg ⁡ S = I