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

Metamath Proof Explorer

Theorem eupth2

Description: The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (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 eupth2 ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 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 eqid ⊢ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩
7 1 2 3 4 5 6 eupthvdres ⊢ ( 𝜑 → ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) = ( VtxDeg ‘ 𝐺 ) )
8 7 fveq1d ⊢ ( 𝜑 → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
9 8 breq2d ⊢ ( 𝜑 → ( 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
10 9 notbid ⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
11 10 rabbidv ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )
12 eupthiswlk ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
13 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
14 5 12 13 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
15 nn0re ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℝ )
16 15 leidd ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝐹 ) )
17 breq1 ⊢ ( 𝑚 = 0 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) ↔ 0 ≤ ( ♯ ‘ 𝐹 ) ) )
18 oveq2 ⊢ ( 𝑚 = 0 → ( 0 ..^ 𝑚 ) = ( 0 ..^ 0 ) )
19 18 imaeq2d ⊢ ( 𝑚 = 0 → ( 𝐹 “ ( 0 ..^ 𝑚 ) ) = ( 𝐹 “ ( 0 ..^ 0 ) ) )
20 19 reseq2d ⊢ ( 𝑚 = 0 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) )
21 20 opeq2d ⊢ ( 𝑚 = 0 → ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ )
22 21 fveq2d ⊢ ( 𝑚 = 0 → ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) = ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) )
23 22 fveq1d ⊢ ( 𝑚 = 0 → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) = ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
24 23 breq2d ⊢ ( 𝑚 = 0 → ( 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) ) )
25 24 notbid ⊢ ( 𝑚 = 0 → ( ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) ) )
26 25 rabbidv ⊢ ( 𝑚 = 0 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } )
27 fveq2 ⊢ ( 𝑚 = 0 → ( 𝑃 ‘ 𝑚 ) = ( 𝑃 ‘ 0 ) )
28 27 eqeq2d ⊢ ( 𝑚 = 0 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ) )
29 27 preq2d ⊢ ( 𝑚 = 0 → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } )
30 28 29 ifbieq2d ⊢ ( 𝑚 = 0 → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) )
31 26 30 eqeq12d ⊢ ( 𝑚 = 0 → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ↔ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) ) )
32 17 31 imbi12d ⊢ ( 𝑚 = 0 → ( ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ↔ ( 0 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) ) ) )
33 32 imbi2d ⊢ ( 𝑚 = 0 → ( ( 𝜑 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ) ↔ ( 𝜑 → ( 0 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) )
34 breq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) ↔ 𝑛 ≤ ( ♯ ‘ 𝐹 ) ) )
35 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 0 ..^ 𝑚 ) = ( 0 ..^ 𝑛 ) )
36 35 imaeq2d ⊢ ( 𝑚 = 𝑛 → ( 𝐹 “ ( 0 ..^ 𝑚 ) ) = ( 𝐹 “ ( 0 ..^ 𝑛 ) ) )
37 36 reseq2d ⊢ ( 𝑚 = 𝑛 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) )
38 37 opeq2d ⊢ ( 𝑚 = 𝑛 → ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ )
39 38 fveq2d ⊢ ( 𝑚 = 𝑛 → ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) = ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) )
40 39 fveq1d ⊢ ( 𝑚 = 𝑛 → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) = ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) )
41 40 breq2d ⊢ ( 𝑚 = 𝑛 → ( 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) ) )
42 41 notbid ⊢ ( 𝑚 = 𝑛 → ( ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) ) )
43 42 rabbidv ⊢ ( 𝑚 = 𝑛 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } )
44 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑃 ‘ 𝑚 ) = ( 𝑃 ‘ 𝑛 ) )
45 44 eqeq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) ) )
46 44 preq2d ⊢ ( 𝑚 = 𝑛 → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } )
47 45 46 ifbieq2d ⊢ ( 𝑚 = 𝑛 → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) )
48 43 47 eqeq12d ⊢ ( 𝑚 = 𝑛 → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ↔ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) )
49 34 48 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ↔ ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) )
50 49 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝜑 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ) ↔ ( 𝜑 → ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ) )
51 breq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) ↔ ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) )
52 oveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 0 ..^ 𝑚 ) = ( 0 ..^ ( 𝑛 + 1 ) ) )
53 52 imaeq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝐹 “ ( 0 ..^ 𝑚 ) ) = ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) )
54 53 reseq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) )
55 54 opeq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ )
56 55 fveq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) = ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) )
57 56 fveq1d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) = ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) )
58 57 breq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) ) )
59 58 notbid ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) ) )
60 59 rabbidv ⊢ ( 𝑚 = ( 𝑛 + 1 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } )
61 fveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑃 ‘ 𝑚 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
62 61 eqeq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
63 61 preq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } )
64 62 63 ifbieq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) )
65 60 64 eqeq12d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ↔ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) )
66 51 65 imbi12d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ↔ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) )
67 66 imbi2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) )
68 breq1 ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) ↔ ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝐹 ) ) )
69 oveq2 ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ 𝑚 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
70 69 imaeq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 𝐹 “ ( 0 ..^ 𝑚 ) ) = ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
71 70 reseq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
72 71 opeq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ )
73 72 fveq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) = ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) )
74 73 fveq1d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) = ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) )
75 74 breq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) ) )
76 75 notbid ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) ) )
77 76 rabbidv ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } )
78 fveq2 ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( 𝑃 ‘ 𝑚 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
79 78 eqeq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
80 78 preq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } )
81 79 80 ifbieq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) )
82 77 81 eqeq12d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ↔ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) )
83 68 82 imbi12d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ↔ ( ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) ) )
84 83 imbi2d ⊢ ( 𝑚 = ( ♯ ‘ 𝐹 ) → ( ( 𝜑 → ( 𝑚 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑚 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑚 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑚 ) } ) ) ) ↔ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) ) ) )
85 1 2 3 4 5 eupth2lemb ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ )
86 eqid ⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 )
87 86 iftruei ⊢ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) = ∅
88 85 87 eqtr4di ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) )
89 88 a1d ⊢ ( 𝜑 → ( 0 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ) ) )
90 1 2 3 4 5 eupth2lems ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) )
91 90 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( 𝜑 → ( ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) )
92 91 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) )
93 33 50 67 84 89 92 nn0ind ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝜑 → ( ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) ) )
94 16 93 mpid ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) )
95 14 94 mpcom ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) )
96 11 95 eqtr3d ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) )