Theorem eupth2lemb

Description: Lemma for eupth2 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	eupth2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	eupth2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	eupth2.g	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
	eupth2.f	⊢ ( 𝜑 → Fun 𝐼 )
	eupth2.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
Assertion	eupth2lemb	⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eupth2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		eupth2.g	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
4		eupth2.f	⊢ ( 𝜑 → Fun 𝐼 )
5		eupth2.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
6		z0even	⊢ 2 ∥ 0
7	1	fvexi	⊢ 𝑉 ∈ V
8	2	fvexi	⊢ 𝐼 ∈ V
9	8	resex	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V
10	7 9	pm3.2i	⊢ ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V )
11		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = 𝑉 )
12	10 11	mp1i	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = 𝑉 )
13	12	eqcomd	⊢ ( 𝜑 → 𝑉 = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ) )
15	14	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) )
16		opiedgfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) )
17	10 16	mp1i	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) )
18		fzo0	⊢ ( 0 ..^ 0 ) = ∅
19	18	imaeq2i	⊢ ( 𝐹 “ ( 0 ..^ 0 ) ) = ( 𝐹 “ ∅ )
20		ima0	⊢ ( 𝐹 “ ∅ ) = ∅
21	19 20	eqtri	⊢ ( 𝐹 “ ( 0 ..^ 0 ) ) = ∅
22	21	reseq2i	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) = ( 𝐼 ↾ ∅ )
23		res0	⊢ ( 𝐼 ↾ ∅ ) = ∅
24	22 23	eqtri	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) = ∅
25	17 24	eqtrdi	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ )
27		eqid	⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ )
28		eqid	⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ )
29	27 28	vtxdg0e	⊢ ( ( 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ∧ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) = 0 )
30	15 26 29	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) = 0 )
31	6 30	breqtrrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
32	31	notnotd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
33	32	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
34		rabeq0	⊢ ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
35	33 34	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ )