Theorem fusgrvtxdgonume

Description: The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in Diestel p. 5. See also remark about equation (2) in section I.1 in Bollobas p. 4. (Contributed by AV, 27-Dec-2021)

	Ref	Expression
Hypotheses	finsumvtxdgeven.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	finsumvtxdgeven.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	finsumvtxdgeven.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	fusgrvtxdgonume	⊢ ( 𝐺 ∈ FinUSGraph → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdgeven.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		finsumvtxdgeven.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		finsumvtxdgeven.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4	1 2	fusgrfupgrfs	⊢ ( 𝐺 ∈ FinUSGraph → ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) )
5	1 2 3	vtxdgoddnumeven	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )
6	4 5	syl	⊢ ( 𝐺 ∈ FinUSGraph → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )