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\leftrightarrow \neg K\in \mathrm{dom}I$$
22	7 21	sylib	$$⊢\phi \to \neg K\in \mathrm{dom}I$$
23		disjsn	$$⊢\mathrm{dom}I\cap \left\{K\right\}=\varnothing \leftrightarrow \neg 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)$$