Metamath Proof Explorer

Theorem eupth2lem3lem6

Description: Formerly part of proof of eupth2lem3 : If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than ( P0 ) and ( PN ) : if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 25-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
trlsegvdeg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
trlsegvdeg.f ⊢ ( 𝜑 → Fun 𝐼 )
trlsegvdeg.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
trlsegvdeg.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
trlsegvdeg.w ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
trlsegvdeg.vx ⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
trlsegvdeg.vy ⊢ ( 𝜑 → ( Vtx ‘ 𝑌 ) = 𝑉 )
trlsegvdeg.vz ⊢ ( 𝜑 → ( Vtx ‘ 𝑍 ) = 𝑉 )
trlsegvdeg.ix ⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
trlsegvdeg.iy ⊢ ( 𝜑 → ( iEdg ‘ 𝑌 ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
trlsegvdeg.iz ⊢ ( 𝜑 → ( iEdg ‘ 𝑍 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
eupth2lem3.o ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
eupth2lem3.e ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
Assertion eupth2lem3lem6 ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ¬ 2 ∥ ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 trlsegvdeg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 trlsegvdeg.f ⊢ ( 𝜑 → Fun 𝐼 )
4 trlsegvdeg.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 trlsegvdeg.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6 trlsegvdeg.w ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
7 trlsegvdeg.vx ⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
8 trlsegvdeg.vy ⊢ ( 𝜑 → ( Vtx ‘ 𝑌 ) = 𝑉 )
9 trlsegvdeg.vz ⊢ ( 𝜑 → ( Vtx ‘ 𝑍 ) = 𝑉 )
10 trlsegvdeg.ix ⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
11 trlsegvdeg.iy ⊢ ( 𝜑 → ( iEdg ‘ 𝑌 ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
12 trlsegvdeg.iz ⊢ ( 𝜑 → ( iEdg ‘ 𝑍 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
13 eupth2lem3.o ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
14 eupth2lem3.e ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
15 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( iEdg ‘ 𝑌 ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
16 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( Vtx ‘ 𝑌 ) = 𝑉 )
17 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑁 ) ∈ V )
18 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ∈ 𝑉 )
19 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ V )
20 simpl ⊢ ( ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) → 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) )
21 20 adantl ⊢ ( ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) )
22 simpr ⊢ ( ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) → 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
23 22 adantl ⊢ ( ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
24 21 23 nelprd ⊢ ( ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ¬ 𝑈 ∈ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
25 df-nel ⊢ ( 𝑈 ∉ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ↔ ¬ 𝑈 ∈ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
26 24 25 sylibr ⊢ ( ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ∉ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
27 neleq2 ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } → ( 𝑈 ∉ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ↔ 𝑈 ∉ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
28 26 27 syl5ibr ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } → ( ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ∉ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
29 28 expd ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } → ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) → ( ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) → 𝑈 ∉ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
30 14 29 syl ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) → ( ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) → 𝑈 ∉ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
31 30 3imp ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ∉ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )
32 15 16 17 18 19 31 1hevtxdg0 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) = 0 )
33 32 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) = ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + 0 ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 eupth2lem3lem1 ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ∈ ℂ )
36 35 addid1d ⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + 0 ) = ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) )
37 36 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + 0 ) = ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) )
38 33 37 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) = ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) )
39 38 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 2 ∥ ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
40 39 notbid ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ¬ 2 ∥ ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
41 fveq2 ⊢ ( 𝑥 = 𝑈 → ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) )
42 41 breq2d ⊢ ( 𝑥 = 𝑈 → ( 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
43 42 notbid ⊢ ( 𝑥 = 𝑈 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
44 43 elrab3 ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) } ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
45 5 44 syl ⊢ ( 𝜑 → ( 𝑈 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) } ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ) )
46 13 eleq2d ⊢ ( 𝜑 → ( 𝑈 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑥 ) } ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ) )
47 45 46 bitr3d ⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ) )
48 47 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ) )
49 20 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) )
50 22 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
51 49 50 2thd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ↔ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
52 neeq1 ⊢ ( 𝑈 = ( 𝑃 ‘ 0 ) → ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ) )
53 neeq1 ⊢ ( 𝑈 = ( 𝑃 ‘ 0 ) → ( 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
54 52 53 bibi12d ⊢ ( 𝑈 = ( 𝑃 ‘ 0 ) → ( ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ↔ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) )
55 51 54 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) )
56 55 pm5.32rd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 = ( 𝑃 ‘ 0 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ 𝑈 = ( 𝑃 ‘ 0 ) ) ) )
57 49 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ¬ 𝑈 = ( 𝑃 ‘ 𝑁 ) )
58 biorf ⊢ ( ¬ 𝑈 = ( 𝑃 ‘ 𝑁 ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ 𝑁 ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ 𝑁 ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ) )
60 orcom ⊢ ( ( 𝑈 = ( 𝑃 ‘ 𝑁 ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ↔ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) )
61 59 60 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) ) )
62 61 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 = ( 𝑃 ‘ 0 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) ) ) )
63 50 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ¬ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
64 biorf ⊢ ( ¬ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ) )
65 63 64 syl ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ) )
66 orcom ⊢ ( ( 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∨ 𝑈 = ( 𝑃 ‘ 0 ) ) ↔ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
67 65 66 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 = ( 𝑃 ‘ 0 ) ↔ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) )
68 67 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ 𝑈 = ( 𝑃 ‘ 0 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) ) )
69 56 62 68 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) ) )
70 eupth2lem1 ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) ) ) )
71 18 70 syl ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 𝑁 ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ 𝑁 ) ) ) ) )
72 eupth2lem1 ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) ) )
73 18 72 syl ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 = ( 𝑃 ‘ 0 ) ∨ 𝑈 = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) ) )
74 69 71 73 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )
75 40 48 74 3bitrd ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑁 ) ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∧ ( 𝑈 ≠ ( 𝑃 ‘ 𝑁 ) ∧ 𝑈 ≠ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) → ( ¬ 2 ∥ ( ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) + ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )