# Metamath Proof Explorer

## Theorem p1evtxdeqlem

Description: Lemma for p1evtxdeq and p1evtxdp1 . (Contributed by AV, 3-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
p1evtxdeq.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
p1evtxdeq.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
p1evtxdeq.fv ${⊢}{\phi }\to \mathrm{Vtx}\left({F}\right)={V}$
p1evtxdeq.fi ${⊢}{\phi }\to \mathrm{iEdg}\left({F}\right)={I}\cup \left\{⟨{K},{E}⟩\right\}$
p1evtxdeq.k ${⊢}{\phi }\to {K}\in {X}$
p1evtxdeq.d ${⊢}{\phi }\to {K}\notin \mathrm{dom}{I}$
p1evtxdeq.u ${⊢}{\phi }\to {U}\in {V}$
p1evtxdeq.e ${⊢}{\phi }\to {E}\in {Y}$
Assertion p1evtxdeqlem ${⊢}{\phi }\to \mathrm{VtxDeg}\left({F}\right)\left({U}\right)=\mathrm{VtxDeg}\left({G}\right)\left({U}\right){+}_{𝑒}\mathrm{VtxDeg}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 p1evtxdeq.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 p1evtxdeq.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 p1evtxdeq.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
4 p1evtxdeq.fv ${⊢}{\phi }\to \mathrm{Vtx}\left({F}\right)={V}$
5 p1evtxdeq.fi ${⊢}{\phi }\to \mathrm{iEdg}\left({F}\right)={I}\cup \left\{⟨{K},{E}⟩\right\}$
6 p1evtxdeq.k ${⊢}{\phi }\to {K}\in {X}$
7 p1evtxdeq.d ${⊢}{\phi }\to {K}\notin \mathrm{dom}{I}$
8 p1evtxdeq.u ${⊢}{\phi }\to {U}\in {V}$
9 p1evtxdeq.e ${⊢}{\phi }\to {E}\in {Y}$
10 1 fvexi ${⊢}{V}\in \mathrm{V}$
11 snex ${⊢}\left\{⟨{K},{E}⟩\right\}\in \mathrm{V}$
12 10 11 pm3.2i ${⊢}\left({V}\in \mathrm{V}\wedge \left\{⟨{K},{E}⟩\right\}\in \mathrm{V}\right)$
13 opiedgfv ${⊢}\left({V}\in \mathrm{V}\wedge \left\{⟨{K},{E}⟩\right\}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)=\left\{⟨{K},{E}⟩\right\}$
14 13 eqcomd ${⊢}\left({V}\in \mathrm{V}\wedge \left\{⟨{K},{E}⟩\right\}\in \mathrm{V}\right)\to \left\{⟨{K},{E}⟩\right\}=\mathrm{iEdg}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)$
15 12 14 ax-mp ${⊢}\left\{⟨{K},{E}⟩\right\}=\mathrm{iEdg}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)$
16 opvtxfv ${⊢}\left({V}\in \mathrm{V}\wedge \left\{⟨{K},{E}⟩\right\}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)={V}$
17 12 16 mp1i ${⊢}{\phi }\to \mathrm{Vtx}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)={V}$
18 dmsnopg ${⊢}{E}\in {Y}\to \mathrm{dom}\left\{⟨{K},{E}⟩\right\}=\left\{{K}\right\}$
19 9 18 syl ${⊢}{\phi }\to \mathrm{dom}\left\{⟨{K},{E}⟩\right\}=\left\{{K}\right\}$
20 19 ineq2d ${⊢}{\phi }\to \mathrm{dom}{I}\cap \mathrm{dom}\left\{⟨{K},{E}⟩\right\}=\mathrm{dom}{I}\cap \left\{{K}\right\}$
21 df-nel ${⊢}{K}\notin \mathrm{dom}{I}↔¬{K}\in \mathrm{dom}{I}$
22 7 21 sylib ${⊢}{\phi }\to ¬{K}\in \mathrm{dom}{I}$
23 disjsn ${⊢}\mathrm{dom}{I}\cap \left\{{K}\right\}=\varnothing ↔¬{K}\in \mathrm{dom}{I}$
24 22 23 sylibr ${⊢}{\phi }\to \mathrm{dom}{I}\cap \left\{{K}\right\}=\varnothing$
25 20 24 eqtrd ${⊢}{\phi }\to \mathrm{dom}{I}\cap \mathrm{dom}\left\{⟨{K},{E}⟩\right\}=\varnothing$
26 funsng ${⊢}\left({K}\in {X}\wedge {E}\in {Y}\right)\to \mathrm{Fun}\left\{⟨{K},{E}⟩\right\}$
27 6 9 26 syl2anc ${⊢}{\phi }\to \mathrm{Fun}\left\{⟨{K},{E}⟩\right\}$
28 2 15 1 17 4 25 3 27 8 5 vtxdun ${⊢}{\phi }\to \mathrm{VtxDeg}\left({F}\right)\left({U}\right)=\mathrm{VtxDeg}\left({G}\right)\left({U}\right){+}_{𝑒}\mathrm{VtxDeg}\left(⟨{V},\left\{⟨{K},{E}⟩\right\}⟩\right)\left({U}\right)$