This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∥ ( 𝐷 ‘ 𝑣 ) } ) )